Logica Tools for Thought   Propositional Logic Proofs Premises Conclusion Proof Editor p q p&q=>r r Fitch p&q q|r Fitch p=>q q=>r p=>r Fitch p=>q m=>p|q m=>q Fitch p=>(q=>r) (p=>q)=>(p=>r) Fitch p=>(q=>p) Fitch (p=>(q=>r))=>((p=>q)=>(p=>r)) Fitch (~p=>q)=>((~p=>~q)=>p) Fitch p ~~p Fitch p=>q ~q=>~p Fitch p=>q ~p|q Fitch ((p=>q)=>p)=>p Fitch ~(p|q) ~p&~q Fitch p|~p Fitch p q=>p Fitch p=>(q=>r) p=>q p=>r Fitch Relational Logic Proofs Premises Conclusion Proof Editor AX:(p(X)&q(X)) AX:p(X)&AX:q(X) Fitch AX:(p(X)=>q(X)) AX:p(X)=>AX:q(X) Fitch AX:(p(X)=>q(X)) AX:(q(X)=>r(X)) AX:(p(X)=>r(X)) Fitch AX:AY:p(X,Y) AY:AX:p(X,Y) Fitch AX:AY:p(X,Y) AX:AY:p(Y,X) Fitch EY:AX:p(X,Y) AX:EY:p(X,Y) Fitch EX:~p(X) ~AX:p(X) Fitch AX:~p(X) ~EX:p(X) Fitch Functional Logic Proofs Premises Conclusion Proof Editor AZ:(p(Z) => ~p(f(Z))) AZ:(~p(Z) => p(f(Z))) AZ:(p(Z) => p(f(f(Z)))) Fitch AZ:(p(Z) <=> q(f(Z))) AZ:(p(Z) <=> r(g(Z))) AZ:(q(f(Z)) => r(g(Z))) Fitch q(a) q(b) AX:(p(X) => q(X)) Fitch r(a) AX:(p(X) => r(s(X))) AX:(q(X) => r(s(X))) AX:(r(X) => p(X) | q(X)) AX:r(X) Fitch p(a) AX:(p(X) => p(f(X))) AX:(p(f(X)) => p(g(X))) AX:p(X) Fitch p(a) AX:AY:(p(X) | p(Y) => p(h(X,Y))) AX:p(X) Fitch p(a) AX:(p(X) => q(f(X))) AX:(q(X) => p(f(X))) AX:(p(X) | q(X)) Fitch p(a) p(s(a)) AX:(p(X) => p(s(s(X)))) AX:p(X) Fitch AX:(p(X) => q(f(X))) AX:(q(X) => p(f(X))) p(a) | q(a) AX:(p(X) | q(X)) Fitch p(a) p(s(a)) AX:(p(X) => p(s(s(X)))) AX:(p(X) | q(X)) Fitch Proofs with Equality Premises Conclusion Proof Editor a=b b=c a=c Fitch a=b p(a) p(b) Fitch AY:Y+0=Y AX:AY:AZ:X+(Y+Z)=(X+Y)+Z AY:0+Y=Y Fitch f(0)=0 AZ:f(Z+1)=f(Z)+((Z+1)+(Z+1)) AZ:f(Z)=Z*(Z+1) Fitch rev(a)=a rev(b)=b AX:AY:rev(cons(X,Y))=cons(rev(Y),rev(X)) AX:rev(rev(X))=X Fitch