%  Systematic construction of semantic tableaux
% 
:- ensure_loaded('../Basis/internal_operators.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/utilities.pl').
:- ensure_loaded('../Basis/input_output.pl').

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

%
%  extend_tableau(+(Formulas, LeftTableau, RightTableau, Constants)
%    Performs one tableau rule:
%    1. check for a pair of contradictory 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, if possible, perform beta rule on some member of
%       Formulas
%    5. otherwise, if possible, perform delta rule on some member of
%       Formulas with a new constant, to be added to Constants
%    6. otherwise, perform gamma rule on some member Formula of
%       Formulas, creating instances of Formula with all constants in
%       Constants
%
extend_tableau((Formulas, closed, empty, _)) :- 
	check_closed(Formulas), !.
extend_tableau((Formulas, open, empty, _)) :- 
	checklist(literal, Formulas), !.
extend_tableau((Formulas, LeftTableau, empty, Constants)) :-
	select(Formula, Formulas, Forms),
	Formula = neg neg Form, !,
	list_to_set([Form| Forms], NewFormulas),
	LeftTableau = (NewFormulas, _, _, Constants),
	extend_tableau(LeftTableau).
extend_tableau((Formulas, LeftTableau, empty, Constants)) :-
	alpha_selection(Formulas, Forms), !,
	list_to_set(Forms, NewFormulas),
	LeftTableau = (NewFormulas, _, _, Constants),
	extend_tableau(LeftTableau).
extend_tableau((Formulas, LeftTableau, RightTableau, Constants)) :-
	beta_selection(Formulas, Forms1, Forms2), !,
	list_to_set(Forms1, NewFormulas1),
	list_to_set(Forms2, NewFormulas2),
	LeftTableau  = (NewFormulas1, _, _, Constants),
	RightTableau = (NewFormulas2, _, _, Constants),
	extend_tableau(LeftTableau),
	extend_tableau(RightTableau).
extend_tableau((Formulas, LeftTableau, empty, Constants)) :-
	delta_selection(Formulas, Forms, Constant), !,
	list_to_set(Forms, NewFormulas),
	LeftTableau = (NewFormulas, _, _, [Constant| Constants]),
	extend_tableau(LeftTableau).
extend_tableau((Formulas, LeftTableau, empty, [])) :- !,
	gensym(a, Constant),
	extend_tableau((Formulas, LeftTableau, empty, [Constant])).
extend_tableau((Formulas, LeftTableau, empty, Constants)) :-
	gamma_selection(Formulas, Forms, Constants), !,
	list_to_set(Forms, NewFormulas),
	(   length(NewFormulas, N),
	    length(Formulas, L),
	    L \= N,
	    LeftTableau = (NewFormulas, _, _, Constants),
	    extend_tableau(LeftTableau)
	;   LeftTableau = open
	).

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

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

%
% basic(+Formula)
%
basic(Formula) :-
	Formula =.. [Op| _],
	Op \= xor,
	Op \= eqv,
	Op \= imp,
	Op \= or,
	Op \= and,
	Op \= neg,
	Op \= sep.

%
%  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), !.

%
%  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), !.

%
%  delta_selection(+Formulas, -NewFormulas, -Constant)
%    NewFormulas is Formulas with a delta formula Formula in Formulas
%    deleted, and an instance of Formula with a new constant Constant
%    added
%
delta_selection(Formulas, [Instance| RemainingFormulas], Constant) :-
	select(Formula, Formulas, RemainingFormulas),
	delta_rule(Formula, X, Matrix), !,
	gensym(a, Constant),
	instance(X, Constant, Matrix, Instance).

%
%  gamma_selection(+Formulas, -NewFormulas, +Constants)
%    A gamma formula Formula in Formulas is selected, and NewFormulas
%    consists of all instances of Formula with constants in Constants,
%    followed by the the members of Formulas other than Formula,
%    followed by Formula, with duplicates removed
%
gamma_selection(Formulas, NewFormulas, Constants) :-
	select(Formula, Formulas, RemainingFormulas),
	gamma_rule(Formula, X, Matrix), !,
	instances(X, Constants, Matrix, Instances),
	append(RemainingFormulas, [Formula], Forms1),
	append(Instances, Forms1, Forms2),
	list_to_set(Forms2, NewFormulas).

%
%  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)).

%
%  delta_rule(+Formula, -Variable, -Matrix)
%    Database of rules for delta operators
%
delta_rule(exists X sep A, X, A).
delta_rule(neg forall X sep A, X, neg A).

%
%  gamma_rule(+Formula, -Variable, -Matrix)
%    Database of rules for gamma operators
%
gamma_rule(forall X sep A, X, A).
gamma_rule(neg exists X sep A, X, neg A).

%
%  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).