% A simple propositional tableau solver

% Formulas are represented by the functors
% disj(F,G), where F and G are formulas
% conj(F,G), where F and G are formulas
% imp(F,G) , where F and G are formulas
% neg(F)   , where F is a formula
% variables are represented by atoms (lower case!)
% e.g.
% disj(a, neg(a)) ̂= A ∨ ¬ A
% imp(a, b)       ̂= A ⇒ B

% Normalize formulas to only include conjunction and negation
simplify(disj(F,G), neg(conj(neg(F1), neg(G1)))) :-
    !, simplify(F, F1), simplify(G, G1).

simplify(imp(F,G), neg(conj(F1, neg(G1)))) :-
    !, simplify(F, F1), simplify(G, G1).

simplify(conj(F, G), conj(F1, G1)) :-
    !, simplify(F, F1), simplify(G, G1).

simplify(neg(F), neg(F1)) :-
    simplify(F, F1).

simplify(X, X).

% The tableau(Con, M) relates a list of 'marked' formulas `Conj` with a Model `M`.
% Formulas are marked with the functors `markF(F)` and `markT(F)` where F is a formula
tableau([markT(conj(A,B)) | Con ], M) :-
    tableau([markT(A), markT(B) | Con], M).

tableau([markF(conj(A,_B)) | Con], M) :-
    tableau([markF(A) | Con], M).

tableau([markF(conj(_A,B)) | Con], M) :-
    tableau([markF(B) | Con], M).

tableau([markT(neg(A)) | Con], M) :-
    tableau([markF(A) | Con], M).

tableau([markF(neg(A)) | Con], M):-
    tableau([markT(A) | Con], M).

tableau([markF(A) | Con], [markF(A) | Con1]) :-
    atom(A),
    tableau(Con, Con1),
    maplist(dif(markT(A)), Con1).
    
tableau([markT(A) | Con], [markT(A) | Con1]) :-
    atom(A),
    tableau(Con, Con1),
    maplist(dif(markF(A)), Con1).
tableau([], []).

% To prove a formula valid, we need to show that its negation has no models
prove(A) :-
    simplify(A, A1),
    not(tableau([markF(A1)], _)).