Z3定理的证明:勾股定理(非线性算术) [英] Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)

问题描述

我定义了一个三角形的3个随机项. Microsoft Z3应该输出:

I define 3 random item of a triangle. Microsoft Z3 should output:

• 约束是否满足要求或输入值无效?
• 所有其他变量均分配给具体值的其他所有三角形项目的模型.

为了约束项，我需要 assert 三角等式-我想从勾股定理((h_c² + p² = b²) ^ (h_c² + q² = a²))开始.

In order to constrain the items i need to assert triangle equalities - i wanted to start out with the Pythagorean Theorem ((h_c² + p² = b²) ^ (h_c² + q² = a²)).

我知道Microsoft Z3解决非线性数学问题的能力有限.但是，即使是一些手动计算器也可以解决如下这样的简化版本:

I know that Microsoft Z3 has only limited capabilities to solve non-linear arithematic problems. But even some hand calculators are able to solve a very simplified version like this:

(set-option :print-success true)
(set-option :produce-proofs true)
(declare-const a Real)
(declare-const b Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert
    (exists
        ((c Real))
        (=
            (+
                (* a a)
                (* b b)
            )
            (* c c)
        )
    )
)
(check-sat)
(get-model)

问题

• 如果给出两个值，是否有办法让Microsoft Z3解决勾股定理?
• 或者:是否有另一个定理证明者能够处理非线性算术的这些情况?

The Question

• Is there a way to get Microsoft Z3 to solve the Pythagorean Theorem if two values are given?
• Or: Is there another theorem prover which is able to handle these case of non-linear arithmetic?

感谢您的帮助-如果不清楚，请发表评论.

Thanks for your help concerning that - If anything is unclear, please comment.

推荐答案

Z3具有用于非线性算术的新求解器(nlsat).它比其他求解器更有效(请参阅本文).新的求解器可以解决无量纲的问题. 但是，新的求解器不支持生成证明.如果我们禁用证明生成，则Z3将使用nlsat并轻松解决问题.根据您的问题，似乎您确实在寻找解决方案，因此禁用证明生成似乎不是问题.

Z3 has a new solver (nlsat) for nonlinear arithmetic. It is more efficient than other solvers (see this article). The new solver is complete for quantifier-free problems. However, the new solver does not support proof generation. If we disable proof generation, then Z3 will use nlsat and easily solve the problem. Based on your question, it seems you are really looking for solutions, thus disabling proof generation does not seem to be an issue.

此外，Z3不会产生近似解(如手动计算器). 它使用精确的表示形式表示实数. 我们还可以要求Z3以十进制表示法显示结果(选项:pp-decimal). 这是您在线上的示例.

Moreover, Z3 does not produce approximate solutions (like hand calculators). It uses a precise representation for real algebraic numbers. We can also ask Z3 to display the result in decimal notation (option :pp-decimal). Here is your example online.

在此示例中，当使用精确表示时，Z3将显示c的以下结果.

In this example, when precise representation is used, Z3 will display the following result for c.

(root-obj (+ (^ x 2) (- 2)) 1)

是说c是多项式x^2 - 2的第一个根. 当我们使用(set-option :pp-decimal true)时，它将显示

It is saying that c is the first root of the polynomial x^2 - 2. When we use (set-option :pp-decimal true), it will display

(- 1.4142135623?)

问号用于指示结果被截断. 注意，结果为负数.但是，它确实是您发布的问题的解决方案. 由于要查找三角形，因此应断言这些常数都>0.

The question mark is used to indicate the result is truncated. Note that, the result is negative. However, it is indeed a solution for the problem you posted. Since, you are looking for triangles, you should assert that the constants are all > 0.

顺便说一句，您不需要存在量词.我们可以简单地使用常量c. 这是一个示例(也可以在在rise4fun上在线):

BTW, you do not need the existential quantifier. We can simply use a constant c. Here is an example (also available online at rise4fun):

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)

这是另一个没有解决方案的示例(也可以通过在rise4fun上在线):

Here is another example that does not have a solution (also available online at rise4fun):

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)

顺便说一句，您应该考虑 Z3的Python接口.它更加用户友好.我链接的教程在Kinematics中提供了示例.他们还使用非线性算法对简单的高中物理问题进行编码.

BTW, you should consider the Python interface for Z3. It is much more user friendly. The tutorial that I linked has examples in Kinematics. They also use nonlinear arithmetic to encode simple high-school physics problems.

这篇关于Z3定理的证明:勾股定理(非线性算术)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！