logic - Bernie-Schonfinkel 类公式到底是什么？

Question

我有一个简单的提议。我想断言严格排序的整数列表中的第一个元素是列表中所有元素的最小值。我定义排序列表的方式是定义一个局部不变量，即每个元素都小于它的下一个元素。我在 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 中设置什么选项，使其仅在有效命题时才接受量化公式？

Answer 1

当一个公式只包含谓词、常量、全称量词而不使用理论(例如算术)时，我们说它属于有效命题片段。找到表示该公式具有 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 没有任何命令行来检查公式是否在有效命题片段中。