z3 - 同等の量指定子を含まない数式

Question

Z3 が量指定子の削除後に同等の式を表示できるかどうかを知りたいです。

例 (exists k) (ixk) = 1 かつ k > 5 は

i > 0 および 5 i - 1 < 0。

ここでは、量指定子 k が削除されています。

これは可能ですか？

ありがとう、カウスタブ。

Answer 1

はい、Z3 は 2 つの式が等しいかどうかをチェックできます。pとqが等しいかどうかを確認します。(not (iff p q))が満足できないかどうかを確認する必要があります。

あなたの例では、非線形演算を使用していますi*k。Z3 の量指定子除去モジュールは、非線形実数演算のサポートが制限されています。これは、完全ではない仮想用語置換に基づいています。ただし、例には十分です。Z3 の量指定子除去モジュールと非線形拡張 (つまり、仮想用語置換) を有効にする必要があります。

Z3 でサンプルをエンコードする方法は次のとおりです: http://rise4fun.com/Z3/rXfi

Answer 2

一般に、量指定子を削除した結果が得られます。たとえば、次のようにrise4funに入力します。

(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)

このケースには非線形演算が含まれており、Z3 は量指定子を削除しません。