3

簡単な提案があります。厳密にソートされた整数のリストの最初の要素は、リスト内のすべての要素の最小値であると断言したいと思います。ソートされたリストを定義する方法は、すべての要素が次の要素よりも小さいというローカル不変量を定義することです。私はZ3で次のように命題を定式化しました-

(set-option :mbqi true)
(set-option :model-compact true)

(declare-fun S (Int) Bool)
(declare-fun preceeds (Int Int) Bool)
(declare-fun occurs-before (Int Int) Bool)

;; preceeds is anti-reflexive
(assert (forall ((x Int)) (=> (S x) (not (preceeds x x)))))

;; preceeds is monotonic
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (and (preceeds x y))))
                                       (not (preceeds y x)))))
;; preceeds is a function
(assert (forall ((x Int) (y Int) (z Int)) (=> (and (S x) (and (S y) (and (S z) (and (preceeds x y)
                                             (preceeds x z)))))
                                             (= y z))))
;; preceeds induces local order
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (preceeds x y)))
                                       (< x y))))

;; preceeds implies occurs-before
(assert (forall ((x Int) (y Int)) (=> (and (and (S x) (S y)) (preceeds x y))
                                             (occurs-before x y))))

;;occurs-before is transitivie
(assert (forall ((x Int)(y Int)(z Int))
  (=> (and (S x) (and (S y) (and (S z)(and (occurs-before x y) (occurs-before y z)))))
    (occurs-before x z))
))             

(declare-const h Int)
(assert (S h))
(assert (forall ((x Int)) (=> (S x) (occurs-before h x))))
(assert (forall ((y Int)) (=> (S y) (< h y))))
(check-sat)
(get-model)

まず、どのクラスの公式が効果的に命題論理であるかを正確に知りたいと思います。私の主張は効果的に命題として分類できますか？第二に、上記の私の定式化は正しいですか？第三に、Z3で、効果的に命題論理である場合にのみ定量化された数式を受け入れるようにするには、どのオプションを設定する必要がありますか？

4

1 に答える 1

3

述語、定数、全称記号のみを含み、理論（算術など）を使用しない場合、式は効果的に命題の断片にあると言います。Exists* Forall*数式に数量詞の接頭辞があり、述語のみを使用するという代替定義を見つけることは非常に一般的です。存在記号は、解釈されていない新しい定数を使用して削除できるため、これらの定義は同等です。詳細については、こちらをご覧ください。

算術を使用するため、アサーションは効果的な命題フラグメントには含まれません。Z3は他のフラグメントを決定できます。Z3チュートリアルには、Z3が決定できるフラグメントのリストがあります。アサーションはリストされているフラグメントのいずれにも含まれていませんが、Z3はそれらおよび他の同様のアサーションを問題なく処理できるはずです。

アサーションの正しさに関して、次の2つのアサーションは満たすことができません。

(assert (S h))
(assert (forall ((y Int)) (=> (S y) (< h y))))

で数量詞をインスタンス化すると、どちらが間違っているかhを推測できます。(< h h)あなたがやろうとしていることがわかります。次の単純なエンコーディングを検討することもできます（単純すぎるかもしれません）。こちらからオンラインでも入手できます。

;; Encode a 'list' as a "mapping" from position to value
(declare-fun list (Int) Int)

;; Asserting that the list is sorted
(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (list i) (list j)))))

;; Now, we prove that for every i >= 0 the element at position 0 is less than equal to element at position i
;; That is, we show that the negation is unsatisfiable with the previous assertion
(assert (not (forall ((i Int)) (=> (>= i 0) (<= (list 0) (list i))))))

(check-sat)

最後に、Z3には、数式が効果的に命題論理に含まれているかどうかを確認するためのコマンドラインがありません。

于 2013-03-24T00:42:59.220 に答える