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 に答える