SMT를 사용하여 용어 간략화

Question

나는 조건을 만족할 수 있는지 확인하기 위해 Z3을 사용 해왔다. 그러나 나는 인간의 소비에 대한 용어를 단순화 할 필요가있다. n이 Int 인 경우 And simplify and (n> 4, n! = 5) to n> 5. Z3에서 또는 다른 도구를 통해이를 수행하는 방법을 아는 사람이 있습니까?

Answer 1

이미 알고 있듯이 Z3에는 API 위에 노출 된 단순화자가 있으며 SMT-LIB에서도 사용할 수 있습니다. rise4fun.com/z3 및 rise4fun.com/z3py에서 Z3에 대한 자습서는 단순화 자의 몇 가지 예를 제공합니다. 그러나 단순화자는 일반 형식 변환을 시도하지 않으므로 원하는 스타일의 결과가 나오지 않습니다. 특히 그것은 함께 그리고 단순화하지 않는 N에> 5.

Answer 2

가능한 대답 (N> 4, N = 5!) :

n = Int('n') 

antecedent = And(n >4, n != 5) 
claim1 = n > 5 

prove(Implies(antecedent, claim1)) 

출력 :

proved