在逻辑惠誉系统上工作

Question

与逻辑和惠誉系统作斗争，

我正在尝试，给定(p⇒-q)和(，q∧p⇒r)和p，使用惠誉系统来证明r。

我该怎么做，有什么建议吗？

Answer 1

END END r)

• p

• ¬q (1 3 Implication Elimination)

• ¬q ^p (2 4

• (2 5 Implication Elimination)

• ¬q)->END

)->END END⇒(p-∧？q)和END (？q和p(1 3隐含消除^p(2 4

• (2 5隐含消除)->END

Answer 2

您也可以尝试其他正式的证明系统，这些系统可以作为计算机实现的校验器使用。使用Isabelle的结构化证明语言，您可以像这样编写证明：

theory Scratch
imports Main
begin

notepad
begin
  assume 1: "p ⟶ ¬ q"
    and 2: "¬ q ∧ p ⟶ r"
    and 3: p
  have "¬ q" using 1 and 3 ..
  then have "¬ q ∧ p" using 3 ..
  with 2 have r ..
end

end

Answer 3

下面的证明使用Klement的惠誉风格的自然演绎证明检查器。规则的解释可以在forallx中找到。

​

​

前三行是前提。第4行来自条件消除(→E)，第5行来自合取介绍(∧I)，最后一行来自条件消除。

参考文献

Kevin Klement的JavaScript/PHP惠誉风格的自然演绎证明编辑器和检查器http://proofs.openlogicproject.org/

P. D. Magnus，Tim Button与J. Robert Loftis的补充由Aaron Thomas-Bolduc，Richard Zach重新混合和修订，forallx Calgary Remix: An Introduction to Formal，2018年冬季。http://forallx.openlogicproject.org/