z3真实存在论

Question

Z3决定非线性真实算术的存在片段吗？ 也就是说，我可以使用它作为决定过程来测试一个 无量词的公式与+和x是否有解决方案吗？

Answer 1

是的，Z3有一个非线性多项式实数算术存在片段的判定过程。当然，该程序是完整的可用资源。这个过程非常昂贵。 This article描述了在Z3中实施的程序。

这里是一个小例子（也可在网上here）：

(declare-const a Real) 
(declare-const b Real) 
(assert (= (^ a 5) (+ a 1))) 
(assert (= (^ b 3) (+ (^ a 2) 1))) 
(check-sat) 
(get-model) 
(set-option :pp-decimal true) ;; force Z3 to display the result in decimal notation 
(get-model) 

这里有一个相关的问题：

• Z3 support for nonlinear arithmetic