/*
Autor: Bratko/MB
Version: JUL 2016
Resolution proof system realized in pattern directed programming paradigm.
The engine looks for patterns (left hand side of "--->") and transforms them.
Covers: Propositional Logic.
As the procedure works with [assert] between tests the system has to be restarted, or
the asserted clauses from the last call have to retracted with: retractall(clause(_)).
Example: translate(~((a=>b)&(b=>c)=>(a=>c))), run.
*/

% 1. Transform sentences into Conjunctive Normal Form

 :- consult('ConjunctiveNormalForm.pl').
 
 
% 2. Interpreter for a basic Pattern Directed Reasoning System:
% on the left hand side we find the pattern, on the right hand side actions to be taken

 :- op( 800, xfx, --->).

% run: execute production rules of the form
% Condition ---> Action until action `stop' is triggered

run:-
  Condition ---> Action,        % A production rule
  test(Condition),              % Precondition satisfied?
  execute(Action).

% test( [ Condition1, Condition2, ...])  if all conditions true

test([]).                     % Empty condition

test([First|Rest]):-          % Test conjunctive condition
  call(First),
  test(Rest).

% execute( [ Action1, Action2, ...]): execute list of actions

execute([ stop]):-  !.         % Stop execution

execute([]):-                 % Empty action (execution cycle completed)
  run.                        % Continue with next execution cycle

execute([First|Rest]):-
  call(First),
  execute(Rest).


% 3. Resolution

:- dynamic clause/1, done/3.

% Contradicting clauses

[clause(X), clause(~X)] ---> [write('result: contradiction found: a valid formula.'),stop].

% Remove a true clause

[clause(C), in(P,C), in(~P,C)]  ---> [retract(C)].

% Simplify a clause with doubly occuring literal

[clause(C), deleteLiteral(P,C,C1), in(P,C1)]  ---> [replace(clause(C), clause(C1))].

% Resolution step, special cases of resolution with a single literal (first parameter)
% "done" expresses that this clause/item has been checked and won't be again

[clause(P), clause(C), deleteLiteral(~P,C,C1), \+ done(P,C,P)] --->
       [assert(clause(C1)), assert(done(P,C,P))].

[clause(~P), clause(C), deleteLiteral(P,C,C1), \+ done(~P,C,P)] --->
       [assert(clause(C1)), assert(done(~P,C,P))].

% Resolution step, general case

[clause(C1), deleteLiteral(P,C1,CA), clause(C2), deleteLiteral(~P,C2,CB), \+ done(C1,C2,P)]  --->
       [assert(clause(CA v CB)), assert(done(C1,C2,P))].

% Finishing rule: no more resolution possible, having not found a contradiction

[] ---> [write('result: no contradiction found: an invalid formula.'),stop].


% deleteLiteral(P,E,E1)
% deleting a disjunctive subexpression P from E gives E1

deleteLiteral(X,X v Y,Y).

deleteLiteral(X,Y v X,Y).

deleteLiteral(X,Y v Z,Y v Z1):- deleteLiteral(X,Z,Z1).

deleteLiteral(X,Y v Z,Y1 v Z):- deleteLiteral(X,Y,Y1).

in(X,X).

in(X,Y):- deleteLiteral(X,Y,_).

% 4. Additional predicates

replace(A,B)  :-               % Replace A with B in database
  retract(A), !,                % Retract once only
  assert(B).