Bernie-Schonfinkel公式是什麼？

我有一個簡單的命題。我想斷言嚴格排序的整數列表中的第一個元素是列表中所有元素的最小值。我定義排序列表的方式是定義一個局部不變量，即每個元素都小於它的下一個元素。我制定了我的建議在以下方式中的Z3 -Bernie-Schonfinkel公式是什麼？

(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中設置什麼選項才能使其接受量化公式，只有當它們是有效命題的時候？

來源

2013-03-23 Gowtham Kaki

我們說當一個公式只包含謂詞，常量，通用量詞並且不使用理論（例如算術）時，它就存在於有效的命題片斷中。找到替代定義很常見，該定義說公式具有Exists* Forall*量詞前綴並僅使用謂詞。這些定義是等價的，因爲可以使用新的未解釋的常量來消除存在量詞。欲瞭解更多信息，請參閱here。

因爲您使用算術，所以您的斷言不在有效的命題片段中。 Z3可以決定其他片段。 Z3 tutorial有一個可以由Z3決定的片段列表。您的斷言不在任何列出的片段中，但Z3應該能夠毫無問題地處理它們和其他類似的斷言。

關於您的斷言的正確性，以下兩個斷言不能滿足。

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

如果我們實例的量詞與h我們可以推論(< h h)哪個是假的。我明白你在做什麼。你也可以考慮下面的簡單編碼（也許它太簡單了）。它也可以在線獲得here。

;; 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-24 00:42:59

Bernie-Schonfinkel公式是什麼？

回答

相關問題