%
%  Construction of semantic tableaux for
%     the propositional calculus.
%

user:file_search_path(common,'../common').
:- ensure_loaded(common(io)).
:- ensure_loaded(common(intext)).

%
%  create(Fml, Tab) - Tab is the tabelau for the formula Fml.
%
%  t(Fmls, Left, Right)
%     Fmls is a list of formula at the root of this tableau and
%     Left and Right are the subtrees (Right ignored for alpha rule).
%     The tableau is constructed by instantiating the logical
%     variables for the subtrees.
%
create_tableau(Fml, Tab) :-
  Tab = t([Fml], _, _), 
  extend_tableau(Tab).

%
%  extend_tableau(t(Fmls, Left, Right) - Perform one tableau rule.
%    1. Check for a pair of contradicatory LITERALS (closed).
%    2. Check if Fmls contains only literals (open).
%    3. Perform an alpha or beta rule on the first element of the list.
%    4. If no rule applies (a literal), move it to the tail of Fmls.
%
extend_tableau(t(Fmls, closed, empty)) :- 
  contains_only_literals(Fmls),
  check_closed(Fmls), !.
extend_tableau(t(Fmls, open,   empty)) :- 
  contains_only_literals(Fmls), !.
extend_tableau(t([neg neg A | Tail], Left,   empty)) :- !,
  Left = t([A | Tail], _, _),
  extend_tableau(Left).
extend_tableau(t([A | Tail], Left,   empty)) :-
  alpha(A, A1, A2), !,
  Left = t([A1, A2 | Tail], _, _),
  extend_tableau(Left).
extend_tableau(t([B | Tail], Left,   Right)) :-
  beta(B, B1, B2), !,
  Left  = t([B1 | Tail], _, _),
  Right = t([B2 | Tail], _, _),
  extend_tableau(Left),
  extend_tableau(Right).
extend_tableau(t([Fml | Tail], Left, Right)) :-
  append(Tail, [Fml], Fmls),
  extend_tableau(t(Fmls, Left, Right)).

%  check_closed(Fmls)
%    Fmls is closed if it contains contradictory formulas.
%  contains_only_literals(Fmls)
%    Traverse Fmls list checking that each is a literal.
%  literal(Fml)
%    Fml is a propositional letter or a negation of one.
%
check_closed(Fmls) :-
  member(F, Fmls), member(neg F, Fmls).

contains_only_literals([]).
contains_only_literals([Fml | Tail]) :-
  literal(Fml),
  contains_only_literals(Tail).

literal(Fml)  :- atom(Fml).
literal(neg Fml) :- atom(Fml).

%  alpha(A1 opr A2, A1, A2)
%  beta(A1 opr A2, A1, A2)
%    Database of rules for each operator.
%
alpha(A1 and A2, A1, A2).
alpha(neg (A1 imp A2), A1, neg A2).
alpha(neg (A1 or A2), neg A1, neg A2).
alpha(A1 eqv A2, A1 imp A2, A2 imp A1).
  
beta(B1 or B2, B1, B2).
beta(B1 imp B2, neg B1, B2).
beta(neg (B1 and B2), neg B1, neg B2).
beta(neg (B1 eqv B2),  neg (B1 imp B2), neg (B2 imp B1)).