A pattern-directed program for simple resolution theorem proving.

Source: PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7.

Program source code: theorem_proving.pl

%  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, _).