%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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: ready.pl                                             %
% Purpose: translation into ready for computation form using %
%   ready/2; lists of formulas can be translated using       %
%   ready_list/2                                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


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

% Translation of an arbitrary formula into a conjunction of formulas
% in ready for computation form. The first argument is the input 
% formula, the variable in the second argument will be matched with 
% the result.
%
% Example:
% ?- ready( neg(a and b) and c, Result).
% Result = (a and b implies false)and c
% Yes 
   
% (A => (B ^ C))* = (A => B)* ^ (A => C)*
ready( A implies (B and C), X and Y) :- !,
  ready( A implies B, X),
  ready( A implies C, Y).

% (A => (B => C))* = ((A ^ B) => C)*
ready( A implies (B implies C), X) :- !,
  ready( (A and B) implies C, X).

% (A => (B v C))* = ((A ^ (B => false)) => C)*
% ...

% (A => -B)* = ((A ^ B) => false)*
% ...

% (A => Q)* = A* => Q, Q atomic or false
ready( A implies Q, X implies Q) :-
  atom( Q), !,  % this includes the case Q = false
  ready( A, X).

% (-A)* = (A => false)*
ready( neg A, X) :- !,
  ready( A implies false, X).

% (A v B)* = ((A => false) => B)*
% ...

% (A ^ B)* = A* ^ B*
ready( A and B, X and Y) :- !,
  ready( A, X),
  ready( B, Y).

% base case: all other formulas stay the same
ready( A, A).


% Translate a list of formulas into a list of formulas in ready
% for computation form.

ready_list( [], []).                       % base case

ready_list( [Head | Tail], List) :-        % recursion step
  ready( Head, ReadyHead),                 % translate head
  conj2list( ReadyHead, ReadyHeadList),    % break up conjunctions
  ready_list( Tail, ReadyTail),            % translate tail
  append( ReadyHeadList, ReadyTail, List). % append results