'双箭头' => 真的意味着'暗示'吗？答案

【问题标题】：does the 'double arrow' => really mean 'implies'?'双箭头' => 真的意味着'暗示'吗？
【发布时间】：2012-07-25 10:48:33
【问题描述】：

有

(=> (f g))

总是和

意思一样

(or (not f) g))

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

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

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

我有this 相当大的模型，它是由 Daniel Jackson 的标记扫描模型生成的，适用于那些愿意亲眼看看的人。

【问题讨论】：

标签： z3 smt

【解决方案1】：

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

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

如果有疑问，您可以使用 Z3 来证明这一点。 The below query 是unsat：

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

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

(assert (not conjecture))
(check-sat)

【讨论】：

谢谢。它确实格式不正确。