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 应该能够毫无问题地处理它们和其他类似的断言。

关于你的断言的正确性，以下两个断言不能满足。

(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 回答