# Theorem proving

## 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.

Program source code: theorem_proving.pl

## Listing

```%  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

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