如何用 Z3 证明器检查涉及一些三角学的定理？

【问题标题】：How to check the theorem that involves some trigonometry with Z3 prover?如何用 Z3 证明器检查涉及一些三角学的定理？
【发布时间】：2019-11-21 10:53:34
【问题描述】：

我正在尝试用 Z3 Theorem Prover 来证明以下命题：

|CA|^2 = |AB|^2 + |BC|^2,
|AB| = cos(alpha),
|BC| = sin(alpha)
  =>
|CA| = 1

我到底在做什么：

(declare-const AB Real)
(declare-const BC Real)
(declare-const CA Real)
(declare-const alpha Real)

(assert  (and (>= AB 0) (>= BC 0) (>= CA 0)) )
(assert  (= (^ CA 2) (+ (^ AB 2) (^ BC 2))) )
(assert  (= AB (cos alpha)) )
(assert  (= BC (sin alpha)) )

(assert (not  (= CA 1) ))

(check-sat)

我预计 unsat 但得到 unknown。我也知道问题集中在函数 sin 和 cos 的部分。

我做错了什么？有没有可能做点什么？

感谢您的帮助！

【问题讨论】：

标签： z3 smt

【解决方案1】：

z3 对sin 和cos 的理解相当有限，我不希望它能够决定所有这些问题。有关这方面的详细讨论，请参阅https://github.com/Z3Prover/z3/issues/680。对于复杂的查询，您得到unknown 作为答案是正常的。

话虽如此，你很幸运！ Z3 实际上可以正确回答您的特定查询；但你必须使用正确的咒语。而不是：

(check-sat)

使用

(check-sat-using qfnra-nlsat)

并且 z3 针对这个问题正确地推断出 unsat。这种形式的 check-sat 告诉 z3 使用内部 nl-sat 引擎进行非线性实数运算。

【讨论】：