formal-methods - 如何使用 Z 表示法证明 (p^q) ^ ( q -> r ) <-> r？

Question

我正在尝试使用 Z 符号来证明逻辑表达式。但是，我是 Z 语言的新手。请帮我证明上面的逻辑表达式。

Answer 1

让我们使用 Z 表示法语言来做这件事，它被用作形式规范的语言。

第一步：引入连词

(p ∧ q) ∧ ( q⇒r)  [ ∧ - elim2]   

第二步：我们将有：

 q ⇒ r  

第三步：我们要让 q 为真：

p ∧ q     [ ∧ - elim2]
------
   q

第四步：使用 q 和 q=>r 我们可以说 r 为真。

有关更多信息，请参阅本书“使用 Z”。