/*  Propositional K tableaus
    Signed version
    December, 2003

    Melvin Fitting

  Propositional operators are: neg, and, or, imp, revimp,
    uparrow, downarrow, notimp and notrevimp.
  Modal operators are: box, dia.
*/

:-op(140, fy, [neg, box, dia]).
:-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow,
    notimp, notrevimp]).

/*  member(Item, List) :- Item occurs in List.
*/

member(X, [X | _]).
member(X, [_ | Tail]) :- member(X, Tail).

/*  remove(Item, List, Newlist) :-
      Newlist is the result of removing all occurrences of
      Item from List.
*/

remove(X, [ ], [ ]).
remove(X, [X | Tail], Newtail) :-
  remove(X, Tail, Newtail).
remove(X, [Head | Tail], [Head | Newtail]) :- 
  remove(X, Tail, Newtail).

/*  conjunctive(X) :- X is a signed alpha formula.
*/

conjunctive(t(_ and _)).
conjunctive(f(_ or _)).
conjunctive(f(_ imp _)).
conjunctive(f(_ revimp _)).
conjunctive(f(_ uparrow _)).
conjunctive(t(_ downarrow _)).
conjunctive(t(_ notimp _)).
conjunctive(t(_ notrevimp _)).

/*  disjunctive(X) :- X is a signed beta formula.
*/

disjunctive(f(_ and _)).
disjunctive(t(_ or _)).
disjunctive(t(_ imp _)).
disjunctive(t(_ revimp _)).
disjunctive(t(_ uparrow _)).
disjunctive(f(_ downarrow _)).
disjunctive(f(_ notimp _)).
disjunctive(f(_ notrevimp _)).

/*  unary(X) :- X is a signed negation,
      or an f-signed constant.
*/

unary(f(neg _)).
unary(t(neg _)).
unary(f(true)).
unary(f(false)).

/*  necessity(X) :- X is a signed nu formula.
*/

necessity(t(box _)).
necessity(f(dia _)).

/*  possibility(X) :- X is a signed pi formula.
*/

possibility(t(dia _)).
possibility(f(box _)).

/*  components(X, Y, Z) :- Y and Z are the components
      of the formula X, as defined in the alpha and
      beta table.
*/

components(t(X and Y), t(X), t(Y)).
components(f(X and Y), f(X), f(Y)).
components(t(X or Y), t(X), t(Y)).
components(f(X or Y), f(X), f(Y)).
components(t(X imp Y), f(X), t(Y)).
components(f(X imp Y), t(X), f(Y)).
components(t(X revimp Y), t(X), f(Y)).
components(f(X revimp Y), f(X), t(Y)).
components(t(X uparrow Y), f(X), f(Y)).
components(f(X uparrow Y), t(X), t(Y)).
components(t(X downarrow Y), f(X), f(Y)).
components(f(X downarrow Y), t(X), t(Y)).
components(t(X notimp Y), t(X), f(Y)).
components(f(X notimp Y), f(X), t(Y)).
components(t(X notrevimp Y), f(X), t(Y)).
components(f(X notrevimp Y), t(X), f(Y)).

/*  component(X, Y) :- Y is the component of the
      unary, necessity, or possibility formula X.
*/

component(f(neg X), t(X)).
component(t(neg X), f(X)).
component(f(true), t(false)).
component(f(false), t(true)).
component(t(box X), t(X)).
component(f(dia X), f(X)).
component(t(dia X), t(X)).
component(f(box X), f(X)).

/*  sharp(A, B) :- the sharp operation applied to branch A
      produces branch B.
*/

sharp([], []).
sharp([Head|Tail], New) :-
  \+ necessity(Head),
  sharp(Tail, New).
sharp([Head|Tail], [NewHead|NewTail]) :-
  necessity(Head),
  component(Head, NewHead),
  sharp(Tail, NewTail).

/*  singleLeftStep(Old, New) :-  New is the result of applying
      a single step of the propositional expansion process to 
      the leftmost branch of Old.  Note: modal rules are not
      applied, and only the left branch is involved.
*/

singleLeftStep([Branch | Rest], New) :-
  member(Formula, Branch),
  unary(Formula),
  component(Formula, Newformula),
  remove(Formula, Branch, Temporary),
  Newbranch = [Newformula | Temporary],
  New = [Newbranch | Rest].

singleLeftStep([Branch | Rest], New) :-
  member(Alpha, Branch),
  conjunctive(Alpha),
  components(Alpha, Alphaone, Alphatwo),
  remove(Alpha, Branch, Temporary),
  Newbranch = [Alphaone, Alphatwo | Temporary],
  New = [Newbranch | Rest].

singleLeftStep([Branch | Rest], New) :-
  member(Beta, Branch),
  disjunctive(Beta),
  components(Beta, Betaone, Betatwo),
  remove(Beta, Branch, Temporary),
  Newbranchone = [Betaone | Temporary],
  Newbranchtwo = [Betatwo | Temporary],
  New = [Newbranchone, Newbranchtwo | Rest].

/*  expandLeft(Old, New) :- New is the result of applying
      singleLeftStep as many times as possible, starting
      with Old.  Thus it produces a left branch on which
      all propositional (but not modal) rules have been
      applied.
*/

expandLeft(Tableau, Newtableau) :-
  singleLeftStep(Tableau, Temp), !,
  expandLeft(Temp, Newtableau).

expandLeft(Tableau, Tableau) .

/*  closedBranch(Branch) :- Branch contains a contradiction.
*/

closedBranch(Branch) :-
  member(t(false), Branch).

closedBranch(Branch) :-
  member(t(X), Branch),
  member(f(X), Branch).

/*  expandAndTest(Tableau) :- expands Tableau and tests for
      closure.  Expansion is always of the leftmost branch.
      Test for left branch closure is performed after all
      propositional rules have been applied, but before a modal
      rule is applied.
*/

expandAndTest([]).
expandAndTest([A|B]) :-
  expandLeft([A|B], [Branch|Rest]),
    (
      (closedBranch(Branch),
       expandAndTest(Rest)
      );
      (member(Pi, Branch),
       possibility(Pi),
       component(Pi, Pizero),
       sharp(Branch, Temp),
       NewBranch = [Pizero|Temp],
       expandAndTest([NewBranch|Rest])
      )
    ).

 /*  if_then_else(P, Q, R) :-
        either P and Q, or not P and R.
*/

if_then_else(P, Q, R) :- P, !, Q.

if_then_else(P, Q, R) :- R.

/*  test(X) :- create a complete tableau expansion
        for f(X), if it is closed, say we have a
        proof, otherwise, say we don't.
*/

test(X) :-
  if_then_else(expandAndTest([[f(X)]]), yes, no).

yes :- write('Propositional K tableau theorem'), nl.

no :- write('Not a propositional K tableau theorem'), nl.