[Albrecht Heeffer]
Home Logic Math Publications Shogi Sites About Me
         
Tableaux-based theorem prover

Tableaux-based theorem prover for CL and paralogics CLuN, CLaN and CLoN

by Albrecht Heeffer

Choose a logic:
Logic: CL CLuN CLaN CLoN

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) :

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 ∨

About ParaLogics:
CLuN is a paraconsistent logic arrived by dropping the consistency requirement 'if v(A) = 1 then v(¬A) = 0' from classical logic.
CLaN is a paracomplete logic derived from CL by dropping the completenes requirement 'if v(A) = 0 then v(¬A) = 1'
CLoN is obtained by dropping both consistency and completeness requirements from classical logic
 

This implementation is based on:
Batens D.; De Clercq K. and Kurtonina N. (1999) "Embedding and interpolation for some paralogics. The propositional case." Reports on Mathematical Logic 33 pp. 29-44.
and help from Alex Klijn.

© 2002 Albrecht Heeffer