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公式是什么？

回答

相关问题