Features     Testimonials     System Requirements     Contact Us     Author's Blog     Home    

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.

Top