邏輯上的工作 - 惠譽系統

Question

與邏輯和惠譽系統掙扎，

我想，鑑於（P⇒¬q）和（¬q∧p⇒r）和P，以使用譽系統證明r。

關於如何進行的任何想法？

Answer 1

1. （P⇒¬q）
2. （¬q∧p⇒R）
3. p
4. ¬q（1所3蘊涵消除）
5. ¬q^ P（2 4與介紹）
6. R（2 5意義消除） ---> END

Answer 2

你也可以嘗試是AVA其他形式證明系統作爲計算機執行的證明檢查員是可用的。使用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