Screen Shots

Fig. 1  Main screen. Display of proof that the AND-operator (&) is commutative.


 Fig. 2  Logic menu. The rules of inference.



  Fig. 3  Premise form. Used here to enter and verify the premise 'P & Q'.


Fig. 4  Substitution form. Used here to substitute 'a' for 'b' on line 2 of a proof.


Fig. 5  Induction Shortcut form. Used here to prove that, for
all natural numbers x, we have ~x=x+1.


Fig. 6  Subset Axiom form. Used here to select a subset r from
the set u such that x is an element of r if and only if x is not
an element of itself.