%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CS2LAP: Logic and Prolog 2000/2001                         %
% Implementation of a Goal-directed Theorem Prover in Prolog %
% Ulle Endriss, King's College London, endriss@dcs.kcl.ac.uk %
%                                                            %
%           *** Partially Finished Version ***               %
%                                                            %
% File: prover.pl                                            %
% Purpose: implement the predicate prover/3 according to     %
%   the goal-directed method; implement output/4, which      %
%   specifies how a proof step is printed on the screen      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% Note: The implementation of prover/3 is not complete. The missing
% clauses are indicated by three dots (...).
 

% The predicate prove/3 implements a (not yet complete) theorem prover
% for formulas in ready for computation form. Each program clause 
% corresponds to one of the goal-directed rules. (The very last one is 
% not really a "rule". It will always be chosen when all other rules 
% failed, put out a message, and then fail itself.)
% The first argument is the list of data formulas and the second one is
% the current goal formula. The history of previous goals (atoms that 
% might be restarted) is kept in the third argument. Initially, this has 
% to be the empty list.
%
% Example (for the complete version):
% ?- prove( [(a and b) implies c, a, b], c, []).
% [a and b implies c, a, b]  |--  c
%   |
%   | rule for atoms
%   |
% [a, b]  |--  a and b
%   |
%   | rule for conjunction
%   |
% [a, b]  |--  a
%   |
%   | success
%   |
% next sub-proof (from rule for conjunction):
% [a, b]  |--  b
%   |
%   | success
%   |
% Yes  

% success
prove( Data, A, History) :-
  atom( A),
  member( A, Data), !,
  output( Data, A, History, 'success').

% success because false in data
% ...

% rule for implication
prove( Data, A implies B, History) :- !,
  output( Data, A implies B, History, 'rule for implication'),
  conj2list( A, As), % antecedent could be a conjunction
  append( Data, As, NewData),
  prove( NewData, B, History).

% rule for conjunction
% (In the output, it should be indicated when the second sub-proof starts.)
% ...

% rule for atoms
prove( Data, B, History) :-
  atom( B),
  member( A implies B, Data), !,
  output( Data, B, History, 'rule for atoms'),
  delete( Data, A implies B, NewData),
  add( B, History, NewHistory),
  prove( NewData, A, NewHistory).

% rule for atoms with A => false
% ...

% restart rule
prove( Data, A, History) :-
  member( B, History),
  (member( B, Data) ; member( _ implies B, Data)), !, % check next step 
  output( Data, A, History, 'restart'),               % is possible
  add( A, History, NewHistory),
  prove( Data, B, NewHistory).

% stuck
prove( Data, Goal, History) :- !, % always matches
  output( Data, Goal, History, 'stuck'), 
  fail. 


% Print out a proof step. The predicate output/4 gets all
% information relevant to any one proof step, namely the current
% list of data formulas, the current goal, the history of goals,
% and the name of the rule used.
% Note that this implementation doesn't use the information on
% the history for the output (but you might want to change this 
% for debugging purposes).

output( Data, Goal, _, Rule) :- !, 
  write( Data), write( '  |--  '), write( Goal), nl,
  write( '  |'), nl,
  write( '  | '), write( Rule), nl,
  write( '  |'), nl.