/* Note: if your implementation of prolog has
copy_term built in, comment out the following
instruction
*/

copy_term(X, Y) :-
  asserta(axiom(X)), retract(axiom(Y)).

/* Further note: the op-codes may need adjustment
for your system.  See below.  In addition, several
Prologs use \+ instead of not.  We use not in one
place below, and it may need replacement.
*/


/* Fixpoint program for GL.  To use, query with
fixedpoint(---, X), where --- is a formula
built up from propositional variables, which
are prolog constants (they start with a lower case
letter) and from X, which is any prolog variable
(it starts with a capital letter).  X represents 
the fixpoint variable.  Use as connectives:
and, or, neg, imp, iff, and modal operators
box and dia.  The binary connectives are infix,
and negation and the modal operators are prefix.

Example:  the query
fixedpoint(neg box Fix, Fix)
returns
dia true

The method derives a fixpoint from an interpolant,
and finds interpolant using semantic tableaus.

Melvin Fitting
June 1995

Revision of 1991.
*/


/*  Propositional operators are: and, or, neg, imp, iff.
And, or are left associative;
iff, imp are right associative.
And there are modal operators, box and dia.

Note: op codes are handled differently on different
systems.  If the following does not work, try
replacing ?- with :-, or leaving it out entirely.
Also some prologs can't manage lists, in which
case neg, box, and dia should be separated, and
similarly for imp and iff.
*/

?-op(100, fy, [neg, box, dia]).
?-op(110, yfx, and).
?-op(120, yfx, or).
?-op(130, xfy, [imp, iff]).

/*  member(X, Y) :- X is a member of
        the list Y.
*/

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

/*  remove(X, Y, Z) :- Z is the list resulting from removing all X
        occurrences from the list Y.
*/

remove(X, [X | Xs], Ys) :- remove(X, Xs, Ys).
remove(Z, [X | Xs], [X | Ys]) :- X \== Z, remove(Z, Xs, Ys).
remove(X, [], []).

/*  Define the propositional formula types,
       for both biased and unbiased formulas.
*/

conjunctive(_ and _).
conjunctive(neg(_ or _)).
conjunctive(neg(_ imp _)).
conjunctive(_ iff _).
conjunctive(left(X)) :- conjunctive(X).
conjunctive(right(X)) :- conjunctive(X).

disjunctive(_ or _).
disjunctive(neg(_ and _)).
disjunctive(_ imp _).
disjunctive(neg(_ iff _)).
disjunctive(left(X)) :- disjunctive(X).
disjunctive(right(X)) :- disjunctive(X).

negative(neg neg _).
negative(left(X)) :- negative(X).
negative(right(X)) :- negative(X).

necessity(box _).
necessity(neg dia _).
necessity(left(X)) :- necessity(X).
necessity(right(X)) :- necessity(X).

possibility(dia _).
possibility(neg box _).
possibility(left(X)) :- possibility(X).
possibility(right(X)) :- possibility(X).

/*  components(F, One, Two) :-
        binary formula F has One and Two
        as its components.  Similarly for
        biased formulas.
*/

components(neg(X and Y), neg X, neg Y).
components(X or Y, X, Y).
components(X and Y, X, Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X iff Y, X imp Y, Y imp X).
components(neg(X iff Y), neg(X imp Y), neg(Y imp X)).

components(left(X), left(Y), left(Z)) :-
    components(X, Y, Z).
components(right(X), right(Y), right(Z)) :-
    components(X, Y, Z).

/*  component(F, One) :-
        unary formula F has One as its only
        component.  Similarly for biased formulas.
*/

component(neg neg X, X).
component(box X, X).
component(neg box X, neg X).
component(dia X, X).
component(neg dia X, neg X).

component(left(X), left(Y)) :-
    component(X, Y).
component(right(X), right(Y)) :-
    component(X, Y).

/*  sharp(X, Y) :-
         Y is the sharped version of the list X.
*/

sharp([], []).

sharp([Nu | Rest], [Nu, Nu_zero | New_rest]) :-
   necessity(Nu),
   component(Nu, Nu_zero),
   sharp(Rest, New_rest).

sharp([Head | Rest], New_rest) :-
   not necessity(Head),
   sharp(Rest, New_rest).

/*  interp(Br, I) :-
       Br is a biased tableau branch and
       I is an interpolant.
*/

interp(Br, I) :-
   member(left(A), Br),
   member(left(neg A), Br),
   I = false.

interp(Br, I) :-
   member(right(A), Br),
   member(right(neg A), Br),
   I = true.

interp(Br, I) :-
   member(left(A), Br),
   member(right(neg A), Br),
   I = A.

interp(Br, I) :-
   member(right(A), Br),
   member(left(neg A), Br),
   I = neg A.

interp(Br, I) :-
   member(DoubleNeg, Br),
   negative(DoubleNeg),
   component(DoubleNeg, Plain),
   remove(DoubleNeg, Br, Temp),
   New_Br = [Plain | Temp],
   interp(New_Br, I).

interp(Br, I) :-
   member(Alpha, Br),
   conjunctive(Alpha),
   components(Alpha, Alpha_one, Alpha_two),
   remove(Alpha, Br, Temp),
   New_Br = [Alpha_one, Alpha_two | Temp],
   interp(New_Br, I).

interp(Br, I) :-
   member(Beta, Br),
   disjunctive(Beta),
   Beta = left(_),
   components(Beta, Beta_one, Beta_two),
   remove(Beta, Br, Temp),
   New_Br_one = [Beta_one | Temp],
   New_Br_two = [Beta_two | Temp],
   interp(New_Br_one, A),
   interp(New_Br_two, B),
   I = (A or B).

interp(Br, I) :-
   member(Beta, Br),
   disjunctive(Beta),
   Beta = right(_),
   components(Beta, Beta_one, Beta_two),
   remove(Beta, Br, Temp),
   New_Br_one = [Beta_one | Temp],
   New_Br_two = [Beta_two | Temp],
   interp(New_Br_one, A),
   interp(New_Br_two, B),
   I = (A and B).

interp(Br, I) :-
   member(Pi, Br),
   Pi = left(Pifmla),
   possibility(Pi),
   component(Pi, Pi_zero),
   remove(Pi, Br, Temp),
   sharp(Temp, Temp_sharp),
   New_Br = [Pi_zero, left(neg Pifmla) | Temp_sharp],
   interp(New_Br, A),
   I = dia A.

interp(Br, I) :-
   member(Pi, Br),
   Pi = right(Pifmla),
   possibility(Pi),
   component(Pi, Pi_zero),
   remove(Pi, Br, Temp),
   sharp(Temp, Temp_sharp),
   New_Br = [Pi_zero, right(neg Pifmla) | Temp_sharp],
   interp(New_Br, A),
   I = box A.

/*  An elementary simplification step.
*/

easysimp(true and X, X).
easysimp(X and true, X).
easysimp(X and false, false).
easysimp(false and X, false).
easysimp(true or X, true).
easysimp(X or true, true).
easysimp(false or X, X).
easysimp(X or false, X).
easysimp(true imp X, X).
easysimp(X imp true, true).
easysimp(false imp X, true).
easysimp(X imp false, neg X).
easysimp(neg true, false).
easysimp(neg false, true).
easysimp(box true, true).
easysimp(box false, box false).
easysimp(dia true, dia true).
easysimp(dia false, false).
easysimp(X, X).

/*  simplify(X, Y) :- Y is the result of applying
       elementary simplifications throughout formula X
       where the only connectives are and, or.
*/

simplify_(X and Y, Z) :- simplify_(X, X1), simplify_(Y, Y1), easysimp(X1 and Y1, Z).
simplify_(X or Y, Z) :- simplify_(X, X1), simplify_(Y, Y1), easysimp(X1 or Y1, Z).
simplify_(box X, Z) :- simplify_(X, X1), easysimp(box X1, Z).
simplify_(dia X, Z) :- simplify_(X, X1), easysimp(dia X1, Z).
simplify_(X, X).

simplify(X, Y) :- simplify_(X, Y), !.

/*  And now, the driver.

  fixedpoint(X, Fix) :- replace Fix in X with ppp getting AP,
       also with qqq getting AQ, from these, form the
       appropriate two formulas, call on interp to compute
       an interpolant, then print it.
*/

fixedpoint(X, Fix) :-
  copy_term((X, Fix), (AP, ppp)),
  copy_term((X, Fix), (AQ, qqq)),
  One = ppp and AP and box(AP imp ppp) and box(ppp imp AP),
  Two = box((AQ imp qqq) and (qqq imp AQ)) imp (AQ or qqq),
  interp([left(One), right(neg Two)], A),
  simplify(A, A1), write(A1), nl, !, fail.