====== Theorem proving ======
{{tag>proof operators}}
===== Description =====
A pattern-directed program for simple resolution theorem proving.

**Source**:  PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7.
===== Download =====
Program source code: {{theorem_proving.pl}}
===== Listing =====
<code prolog>
%  Figure 23.15  A pattern-directed program for simple resolution
%  theorem proving.

:- op( 900, fy, not).
:- op( 800, xfx, --->).
:-  op( 120, xfy, v). 
:-  op( 100, fy, ~).        % Negation

% not Goal): negation as failure; 
%   Note: This is often available as a built-in predicate,
%   often written as prefix operator "\+", e.g. \+ likes(mary,snakes)

not Goal  :-
  Goal, !, fail
  ; 
  true.

% The following directive is required by some Prologs

:- dynamic clause/1, done/3.

% Production rules for resolution theorem proving

% Contradicting clauses

[ clause( X), clause( ~X) ] --->
[ write('Contradiction found'), stop].

% Remove a true clause

[ clause( C), in( P, C), in( ~P, C) ]  --->
[ retract( C) ].

% Simplify a clause

[ clause( C), delete( P, C, C1), in( P, C1) ]  --->
[ replace( clause( C), clause( C1)) ].

% Resolution step, a special case

[ clause( P), clause( C), delete( ~P, C, C1), not done( P, C, P) ] --->
[ assert( clause( C1)), assert( done( P, C, P)) ].

% Resolution step, a special case

[ clause( ~P), clause( C), delete( P, C, C1), not done( ~P, C, P) ] --->
[ assert( clause( C1)), assert( done( ~P, C, P)) ].

% Resolution step, general case

[ clause(C1), delete( P, C1, CA),
  clause(C2), delete( ~P, C2, CB),  not done( C1,C2,P) ]  --->
[ assert( clause(CA v CB)), assert( done( C1, C2, P)) ].

% Last rule: resolution process stuck

[] ---> [ write('Not contradiction'), stop].


% delete( P, E, E1)  if
%   deleting a disjunctive subexpression P from E gives E1

delete( X, X v Y, Y).

delete( X, Y v X, Y).

delete( X, Y v Z, Y v Z1)  :-
  delete( X, Z, Z1).

delete( X, Y v Z, Y1 v Z)  :-
  delete( X, Y, Y1).

% in( P, E)  if P is a disjunctive subexpression in E

in( X, X).

in( X, Y)  :-
  delete( X, Y, _).
</code>
===== Comments =====