gpt4 book ai didi

logic - Z3定理证明者 : Pythagorean Theorem (Non-Linear Artithmetic)

转载 作者:行者123 更新时间:2023-12-02 08:23:15 25 4
gpt4 key购买 nike

为什么?

我的问题发生的用例上下文

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

  • 是否满足约束条件或者是否存在无效的输入值?
  • 所有其他三角形项目的模型,其中所有变量都分配给具体值。

为了约束我需要断言三角形等式的项目 - 我想从毕达哥拉斯定理开始((h_c² + p² = b²) ^ (h_c² + q² = a²))。

问题

我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手持计算器也能够解决非常简化的版本,如下所示:

(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 求解毕达哥拉斯定理?
  • 或者:是否有另一个定理证明器能够处理这些非线性算术情况?

感谢您对此的帮助 - 如果有任何不清楚的地方,请发表评论。

最佳答案

Z3 有一个用于非线性算术的新求解器 (nlsat)。它比其他求解器更高效 ( see this article )。新的求解器对于无量词问题来说是完整的。然而,新的求解器不支持证明生成。如果我们禁用证明生成,那么 Z3 将使用 nlsat 并轻松解决问题。根据您的问题,您似乎确实在寻找解决方案,因此禁用证明生成似乎不是问题。

此外,Z3 不产生近似解(如手持计算器)。它使用实代数数的精确表示。我们还可以要求 Z3 以十进制表示法显示结果(选项 :pp-decimal)。 Here is your example online .

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

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

也就是说,c 是多项式x^2 - 2 的第一个根。当我们使用(set-option :pp-decimal true)时,会显示

(- 1.4142135623?)

问号用于表示结果被截断。请注意,结果是否定的。不过,这确实是您发布的问题的解决方案。由于您正在寻找三角形,因此您应该断言常数都 > 0。

顺便说一句,您不需要存在量词。我们可以简单地使用常量c。这是一个示例(也可用 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)

这是另一个没有解决方案的示例(也可用 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)

顺便说一句,您应该考虑 Python interface for Z3 。它更加用户友好。我链接的教程有运动学方面的示例。他们还使用非线性算术来编码简单的高中物理问题。

关于logic - Z3定理证明者 : Pythagorean Theorem (Non-Linear Artithmetic),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15110692/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com