1

做

(=> (f g))

总是意味着同样的事情

(or (not f) g))

?

这两个表达式在我的模型中表现不同。虽然使用=>给了我UNSAT，但使用其他变体不会产生任何结果（timeout）。我会满足于拥有一个运算符列表及其含义。我知道 SMTLIB 标准，但文档没有明确讨论运算符的含义。具体来说，如果在三元表达式中使用，' => ' 似乎可以兼作 ' ite ' (if_then_else) 运算符的别名，我对此感到非常困惑。

如果相关，我设置了AUFLIA逻辑。

我正在寻找一个简单的是或否的答案。其次是关于 SMT2 的适当文档（可能是一本书）。

我有这个相当大的模型，这个模型是从 Daniel Jackson 的标记扫描模型生成的，用于那些愿意亲眼看看的人的合金 4。

4

1 回答 1

2

您的表达不正确/格式不正确。

=>确实意味着“暗示”。换句话说，(=> f g)等价于(or (not f) g)。

如果有疑问，您可以使用 Z3 来证明它。以下查询是unsat：

(declare-const p Bool)
(declare-const q Bool)

(define-fun conjecture () Bool
    (= (=> p q) 
       (or (not p) q)))

(assert (not conjecture))
(check-sat)
于 2012-07-25T11:08:53.543 回答