%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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: main.pl                                              %
% Purpose: define operators; compile all other files;        %
%   implement main predicate prove/2                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% Note: You don't have to make any changes to this file.


% Define logic operators for propositional logic.

:- op( 100, fy, neg),
   op( 200, yfx, and),
   op( 300, yfx, or),
   op( 400, yfx, implies).


% Compile the other three program files as soon as this file is
% being consulted.

:- consult( auxiliary), % some auxiliary predicates
   consult( prover),    % the core of the theorem prover
   consult( ready).     % translation into ready for computation form


% The main predicate prove/2. Given a list of data formulas in the 
% first argument and a goal formula in the second argument this
% predicate will succeed, if and only if the respective argument is
% valid. All prove steps undertaken to show this will be printed out 
% on the screen. The first of these steps is the rewriting of goal
% and data in ready for computation form.
%
% Example:
%
% ?- prove( [a implies b, neg b], neg a).
%   |
%   | rewrite in ready for computation form
%   |
% [a implies b, b implies false]  |--  a implies false
%   |
%   | rule for implication
%   |
% [a implies b, b implies false, a]  |--  false
%   |
%   | rule for atoms
%   |
% [a implies b, a]  |--  b
%   |
%   | rule for atoms
%   |
% [a]  |--  a
%   |
%   | success
%   |
% Yes         
%
% Note that this predicate will work correctly only after you have 
% completed the files prover.pl and ready.pl.  

prove( Data, Goal) :-
  ready_list( Data, ReadyData),      % rewrite data   
  ready( Goal, ReadyGoal),           % rewrite goal
  write( '  |'), nl,
  write( '  | rewrite in ready for computation form'), nl,
  write( '  |'), nl,
  prove( ReadyData, ReadyGoal, []).  % start proof