 # proof.p

```%  =================================================================
%  ==                                                             ==
%  ==          An Introduction to ARTIFICIAL INTELLIGENCE         ==
%  ==                  Janet Finlay and Alan Dix                  ==
%  ==                       UCL Press, 1996                       ==
%  ==                                                             ==
%  =================================================================
%  ==                                                             ==
%  ==        chapter 3, pages 53-54:  addition proof graph        ==
%  ==                   pages 62-63:  closed lists                ==
%  ==                                                             ==
%  ==            Prolog example, Alan Dix, August 1996            ==
%  ==                                                             ==
%  =================================================================```

### Code

```%  The addition proof graph can be represnted extensionally
%  as in hanext.pl, but instead we will simply represent
%  general proof rules for addition:

%  This looks too good to be true, almost quoting
%  the laws from the book!
%  This is because Prolog very kindly matches expressions
%  like x+(y+z) for us.
%
%  Note that when you enter something like x+y, or even X+Y,
%  Prolog does not do the arithmatic.  Instead, it simply
%  constructs a representation of the expression.

%  However, one extra rule is needed.  The commutative law is reflexive,
%  but the associative law really needs a second law of the form:

%  to allow it to work in both directions.
%
%  Alternatively, we could have added a general rule of the form:
%  This says that if law R says that X=Y then it also means
%  that Y=X  -  equality is symmetric.
%  and would need additional rukles to prevent this.
%  So we'll stick to using associative law 2

%  Given such laws we can write a predicate which proves
%  such laws and keeps track of the train of reasoning:

write('looking at '), write(Next), nl,

%  It is designed to generate proofs of the form:
%          [x+(y+z),c,(y+z)+x,a,y+(z+x)]

%  What is wrong with it?

%  Try running it to see - the 'write's will let
%  you see what is going on.

%  To make it work we need a 'closed list' (see pages 62/63) to
%  stop us stuttering.

write('looking at '), write(Next), nl,
\+ member(Next,Closed),
write('not seen before'), nl,

%  The closed list stops it revisiting the same state and Prolog's
%  backtracking allows it to lok at alternative prrof paths when
%  it gets stuck.  This is a form of depth-first search
%  (see section 3.2.1, page 55 on).

```

### Running this Code

```%  RUNNING THIS CODE
%
%  Try the example in the book:
%
%
%  Note the closed list starts off as the start state - the only
%  place you have visited so far.
%

%  The proof engine would work for any equality type proofs.
%  For example, we could include multiplication rules like:
%
%    adding_law(am,L*(M*N),(L*M)*N).  %  associativity of multiplication
%    adding_law(cm,M*N,N*M).          %  commutativity of multiplication
%

%  Two sorts of problem prevent this being able to solve all
%  mathematics (!)

%  First, some more general mathematical things need to be added.
%  For example, at the moment it doesn't look 'inside' brackets,
%  so it can't probe that x+(y+z)=x+(z+y)
%
%  This is not too difficult to solve - it needs some rules such as:

%
%  This says that if X=Z then X+Y=X+Z

%  More fundamental is that the search space becomes very big.
%  Some things can be solved by brute force, but more difficult
%  problems require some insight.  Real automatic proof systems
%  include many heuristics, rules to help guide the proof along
%  (hopefully) fruitful lines.  This includes things like "bring
%  like terms together" so that they can cancel out or be grouped
%  together.

```

### Examples

```%  EXAMPLES
%
```
`%>  adding_proof(x+(y+z),y+(z+x),Proof,[x+(y+z)]).`