Z3 无法检查谓词逻辑中的推理，例如 Lewis Carroll 的 SYMBOLIC LOGIC

Question

; All rabbits, that are not greedy, are black
; No old rabbits are free from greediness
; Therefore: Some black rabbits are not old
(declare-sort U) 
(declare-fun g (U) Bool)
(declare-fun b (U) Bool)
(declare-fun o (U) Bool) 
(assert (forall ((x U)) (=> (not (g x)) (b x) ))) 
(assert (forall ((x U)) (=> (o x) (g x) ))) 
(assert (not (exists ((x U)) (and (b x) (not (o x))))))
(check-sat)
; returns sat

我正在检查前提蕴含结论（断言否定）的合取重言式以及前提集与结论否定的矛盾。说，对于矛盾，我期望 unsat

Answer 1

让我们看一下z3返回的模型。你可以通过坚持来实现这一点：

(get-model)

在你的

(check-sat)

之后。如果你这样做，z3 打印：

sat
(
  ;; universe for U:
  ;;   U!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun U!val!0 () U)
  ;; cardinality constraint:
  (forall ((x U)) (= x U!val!0))
  ;; -----------
  (define-fun g ((x!0 U)) Bool
    true)
  (define-fun b ((x!0 U)) Bool
    false)
  (define-fun o ((x!0 U)) Bool
    false)
)

这有点啰嗦。但它本质上说：(1) 想象一个只有一只兔子的世界。 (2) 所有的兔子都是

greedy

。 (3) 没有兔子是

black

。 (4) 没有兔子是

old

.

这样一想，确实满足了你的约束条件。那么，这是怎么回事？这是将“英语”翻译成“正式”逻辑的典型做法。通常情况下，有一些隐含的约束在自然语言中是不言而喻的。事实上，这里也是如此。隐含的是“有些兔子不贪婪”，你没有在形式化中捕捉到。如果我们添加这个：

(assert (exists ((x U)) (not (g x))))

然后z3确实会说

unsat

；如你所料。