[Albrecht Heeffer]
Home Logic Math Publications Shogi Sites About Me
         
Goal-directed theorem prover

Goal-directed theorem prover for CL and paraconsistent logic CLuN

by Albrecht Heeffer

for proving:
{p ∧ (q ∨ r), (q ∧ r) ≡ p, s} |- ¬(q ⊃ ¬s), use
[p&(q v r), (q&r)<=>p, s], -(q=> -s)
Premisses:Conclusion:

Press submit for getting the proof of this example, or edit the input fields for a different proof

For proving a theorem ((p∧~p)∨(q∧~q))∨(((r⊃(p∨q)∧(~p∧~q))⊃~r) : (example in CLuN):

Press submit for getting the proof of this theorem or edit the input fields first for a different proof.
Some guidelines:
'-' is classic negation ¬
'~' is paraconsistent negation
Always use a space before a '-' and '~'
For '¬¬p', use brackets: -(-p)
use a space before and after disjunction ∨
 
© 2002 Albrecht Heeffer