0

引理：forall x : R, x <> 0 -> (x / x) = 1。

证明：

(declare-const x Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (not (= (/ x x) 1)))
(check-sat)

输出是：

unsat

Qed。

引理：forall xy : R, x <> 0, y <> 0 -> (x / x + y / y) = 2。

证明：

(declare-const x Real)
(declare-const y Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (or (> y 0) (< y 0)))
(assert (not (= (+ (/ x x) (/ y y)) 2)))
(check-sat)

输出是：

unsat

Qed。

引理：forall xy : R, x <> 0, y <> 0 -> (x / x + x / y) = ((x + y) / y)。

证明：

(declare-const x Real)
(declare-const y Real)
(push)
(assert (or (> x 0) (< x 0)))
(assert (or (> y 0) (< y 0)))
(assert (not (= (+ (/ x x) (/ x y)) (/ (+ x y) y))))
(check-sat)

输出是：

unsat

Qed。

这些引理是使用 Coq + Maple 在

http://coq.inria.fr/V8.2pl1/contribs/MapleMode.Examples.html

并在网上使用 Z3Py

在线使用 Z3Py 的一些有效性证明和 Nikolaj Bjorner 提出的策略

请让我知道我使用 Z3 SMT 2.0 的证明是否正确，以及您是否知道使用 Z3 SMT 2.0 证明它们的更直接形式。非常感谢。

4

1 回答 1

2

您的编码没有任何问题。您还可以考虑以下更接近您要证明的引理的编码（也可在此处在线获得）：

(assert (not (forall ((x Real)) (=> (not (= x 0)) (= (/ x x) 1)))))
(check-sat)

(reset)
(assert (not (forall ((x Real) (y Real)) (=> (and (not (= x 0))
                                                  (not (= y 0)))
                                             (= (+ (/ x x) (/ y y)) 2)))))
(check-sat)

(reset)
(assert (not (forall ((x Real) (y Real)) (=> (and (not (= x 0))
                                                  (not (= y 0)))
                                             (= (+ (/ x x) (/ x y)) (/ (+ x y) y))))))
(check-sat)
于 2013-05-04T18:10:38.923 回答