2

次のようなものをアサートするSMTLIB2でステートメントを作成する方法に行き詰まっています

forall x < 100, f(x) = 100

このプロパティは、100 未満のすべての数値に再帰的に 1 を追加する関数をチェックします。

(define-fun-rec incUntil100 ((x Int)) Int  
    (ite 
        (= x 100) 
        100
        (incUntil100 (+ x 1))
    )
)

量指定子とパターンに関する Z3 のチュートリアルを読みましたが、あまり理解できなかったようです。

4

1 に答える 1

2

SMTLib では、そのプロパティを次のように記述します。

(assert (forall ((x Int)) (=> (< x 100) (= (incUntil100 x) 100))))
(check-sat)

しかし、これを試してみると、z3 が永久にループし、CVC4 がunknown答えとして教えてくれることがわかります。SMTLib でこれらの種類の関数を定義してアサートすることはできますが、実際の証明に対するソルバーのサポートは、すぐに使用できる帰納法を行わないため、かなり弱いものです。

再帰関数の特性を証明することが目的の場合、SMT ソルバーは適切な選択ではありません。代わりに、Isabelle、HOL、Coq、Lean、ACL2 などの定理証明者を調べてください。まさにその目的のために構築されています。

于 2021-04-14T22:30:17.483 に答える