如何使用 Z3 证明器检查涉及某些三角函数的定理？

Question

我正在尝试用 Z3 定理证明器 证明以下命题：

|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.

的部分

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

感谢帮助！

Answer 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 引擎进行非线性实数运算。

如何使用 Z3 证明器检查涉及某些三角函数的定理？

How to check the theorem that involves some trigonometry with Z3 prover?

smt

z3