/* SIMPLE.

Using PROLOG as a theorem prover:
An equality axioms example.
Try goal 'equal(y,x).'.

Alan Bundy  16.6.81 */


equal(x,y).             % The Hypothesis

equal(X,X).             % The Reflexive Axiom

equal(U,W) :- equal(U,V), equal(W,V).   % The Twisted Transitivity Axiom


/* MINI-PROJECTS

1. Try goal ?- equal(y,x).

2.  Experiment by switching the order of the above axioms and trying
the same goal.  What sort of bad behaviour emerges?  How could it be
avoided?

3. Experiment with different axioms, e.g. the group theory example
from p92 of 'Artificial Mathematicians'.

*/