%  Two constructions of semantic tableaux:
%    1. create_tableau
%    2. create_systematic_tableau
% 
:- ensure_loaded('../Basis/internal_operators.pl').
:- use_module('../Basis/translations.pl').
:- ensure_loaded('../Basis/input_output.pl').

%
%  create_tableau(+Formula, -Tableau)
%    Tableau is a term of the form
%    (ListOfFormulas, LeftTableau, RightTableau),
%    where ListOfFormulas is initialized to [Formula];
%    Tableau is constructed by instantiating the logical
%    variables for LeftTableau and RightTableau
%    (RightTableau is ignored for alpha rule)
%
create_tableau(Formula, Tableau) :-
	Tableau = ([Formula], _, _), 
	extend_tableau(Tableau).

%
%  extend_tableau(+(Formulas, LeftTableau, RightTableau)
%    Performs one tableau rule:
%    1. check for a pair of contradicatory literals (branch is closed)
%    2. check if Formulas contains only literals (branch is open)
%    3. extract first element Formula of Formulas
%    4. If Formula is not a literal, perform an alpha or beta rule
%    5. otherwise, move Formula to the tail of Formulas
%
extend_tableau((Formulas, Conclusion, empty)) :- 
	checklist(literal, Formulas), !,
	(   check_closed(Formulas), !,
	    Conclusion = closed
	;   Conclusion = open
	).
extend_tableau(([neg neg Formula| Formulas], LeftTableau, empty)) :- !,
	LeftTableau = ([Formula| Formulas], _, _),
	extend_tableau(LeftTableau).
extend_tableau(([Formula| Formulas], LeftTableau, empty)) :-
	alpha_rule(Formula, Form1, Form2), !,
	LeftTableau = ([Form1, Form2| Formulas], _, _),
	extend_tableau(LeftTableau).
extend_tableau(([Formula| Formulas], LeftTableau, RightTableau)) :-
	beta_rule(Formula, Form1, Form2), !,
	LeftTableau  = ([Form1| Formulas], _, _),
	RightTableau = ([Form2| Formulas], _, _),
	extend_tableau(LeftTableau),
	extend_tableau(RightTableau).
extend_tableau(([Formula| Formulas], LeftTableau, RightTableau)) :-
	append(Formulas, [Formula], NewFormulas),
	extend_tableau((NewFormulas, LeftTableau, RightTableau)).

%
% literal(+Formula)
%
literal(Formula)  :-
	atom(Formula).
literal(neg Formula) :-
	atom(Formula).

%
%  check_closed(+Formulas)
%
check_closed(Formulas) :-
	member(Formula, Formulas),
	member(neg Formula, Formulas).

%
%  alpha_rule(+A1 operator A2, -A1, -A2)
%    Database of rules for alpha operators
%
alpha_rule(A1 and A2, A1, A2).
alpha_rule(neg (A1 imp A2), A1, neg A2).
alpha_rule(neg (A1 or A2), neg A1, neg A2).
alpha_rule(A1 eqv A2, A1 imp A2, A2 imp A1).
  
%
%  beta_rule(+B1 operator A2, -B1, -B2)
%    Database of rules for beta operators
%
beta_rule(B1 or B2, B1, B2).
beta_rule(B1 imp B2, neg B1, B2).
beta_rule(neg (B1 and B2), neg B1, neg B2).
beta_rule(neg (B1 eqv B2), neg (B1 imp B2), neg (B2 imp B1)).

%
%  write_tableau(+Tableau)
% 
write_tableau(Tableau) :-
	write_tableau(Tableau, 0).

%  write_tableau(+Tableau, +Indent)
%    Write Tableau, indenting each level of the tree by Indent
%
write_tableau(empty, _).
write_tableau(closed, _) :- 
	write('   Closed').
write_tableau(open, _) :- 
	write('   Open').
write_tableau((Formulas, LeftTableau, RightTableau), Indent) :-
	nl, tab(Indent),
	maplist(from_internal_to_printable, Formulas, PrintableFormulas),
	write_formula_list(PrintableFormulas),
	NewIndent is Indent + 3,
	write_tableau(LeftTableau, NewIndent),        
	write_tableau(RightTableau, NewIndent).

%
%  create_systematic_tableau(+Formula, -Tableau)
%    Tableau is a term of the form
%    (ListOfFormulas, LeftTableau, RightTableau),
%    where ListOfFormulas is initialized to [Formula];
%    Tableau is constructed by instantiating the logical
%    variables for LeftTableau and RightTableau
%    (RightTableau is ignored for alpha rule)
%
create_systematic_tableau(Formula, Tableau) :-
	Tableau = ([Formula], _, _), 
	extend_systematic_tableau(Tableau).

%
%  extend_systematic_tableau(+(Formulas, LeftTableau, RightTableau)
%    Performs one tableau rule:
%    1. check for a pair of contradicatory formulas (branch is closed)
%    2. check if Formulas contains only literals (branch is open)
%    3. if possible, perform an alpha rule on some member of Formulas
%    4. otherwise, perform beta rule on some member of Formulas
%
extend_systematic_tableau((Formulas, closed, empty)) :- 
	check_closed(Formulas), !.
extend_systematic_tableau((Formulas, open, empty)) :- 
	checklist(literal, Formulas), !.
extend_systematic_tableau((Formulas, LeftTableau, empty)) :-
	alpha_selection(Formulas, NewFormulas), !,
	LeftTableau = (NewFormulas, _, _),
	extend_systematic_tableau(LeftTableau).
extend_systematic_tableau((Formulas, LeftTableau, RightTableau)) :-
	beta_selection(Formulas, Forms1, Forms2), !,
	LeftTableau  = (Forms1, _, _),
	RightTableau = (Forms2, _, _),
	extend_systematic_tableau(LeftTableau),
	extend_systematic_tableau(RightTableau).

%
%  alpha_selection(+Formulas, -NewFormulas)
%    NewFormulas is Formulas with an alpha formula in Formulas deleted,
%    and the corresponding formulas alpha1 and alpha2 added
%
alpha_selection(Formulas, [Form1, Form2| Forms]) :-
	select(Formula, Formulas, Forms),
	alpha_rule(Formula, Form1, Form2), !.
alpha_selection(Formulas, [Form| Forms]) :-
	select(Formula, Formulas, Forms),
	Formula = neg neg Form.

%
%  beta_selection(+Formulas, -NewFormulas1, -NewFormulas2)
%    NewFormulas is Formulas with a beta formula in Formulas deleted,
%    and one of the corresponding formulas beta1 or beta2 added
%
beta_selection(Formulas, [Form1| Forms], [Form2| Forms]) :-
	select(Formula, Formulas, Forms),
	beta_rule(Formula, Form1, Form2), !.