SWISH -- SWI-Prolog for SHaring

/*
16TaP---Tableaux for 16-valued Trilattice Logic
Reinhard Muskens

16TaP is a simple propositional tableau prover/model generator for a
functionally complete extension of the 16-valued Shramko-Wansing
logic. The prover implements the tableau calculus PL_{16} defined in 
Reinhard Muskens and Stefan Wintein, Analytic Tableaux for all of 
SIXTEEN_3, Journal of Philosophical Logic 44 (5):473-487 (2015)
(http://link.springer.com/article/10.1007/s10992-014-9337-3). It is
loosely based on Beckert and Posegga's LeanTaP prover for predicate
logic, but unlike that little marvel it is not very lean.

The calculus is based on signed formulas and there are eight signs,
which we represent here as, n1, f1, t1, b1, n0, f0, t0, and
b0. Intuitively, 'n1:F' means 'n is an element of the value of F' and
'n0:F' stands for 'n is not an element of the value of F'. A similar
interpretation can be given to the other signs.

There are several notions of entailment that are modelled by the
calculus, and in fact the notions of entailment that are of most
interest, for example those corresponding to one of the orderings in
the trilattice SIXTEEN_3, can be obtained as the intersections of
certain sets of auxiliary entailment relations that the calculus can
characterize. Checking whether a sequence is correct often involves
making several tableaux---four if an entailment relation based on one
of the orderings in the trilattice is considered, and six when a
natural notion of entailment based on two of these orderings is in
focus.

The calculus is based on a functionally complete set of connectives,
which we write here as {nt, nf, ni, at, af, ai, ot, of, oi}. The
connectives whose names start with 'n' are negations; one for the
truth lattice ('t'), one for the (non-)falsity lattice ('f'), and one
for the information lattice ('i'). The other connectives are
conjunctions (names starting with 'a') and disjunctions ('o').

Unlike LeanTaP, the prover does not presuppose that formulas are in
negation normal form. Counterexamples to an argument are given if they
exist and graphical representations of the tableaux that are generated
are given. If a tableau branch is closed, this is marked with an
'x'; open branches are marked with an 'o'.

Speed of execution or compactness of code have not been primary aims
in writing this prover/generator. The basic aims of the program are
demonstration of the calculus and providing a tool for further
analysis of the logic.

As in Beckert and Posegga's LeanTap, the prover searches through the
branches of a tableau in Prolog's left-right depth-first manner.
*/

:- use_rendering(svgtree).

/*
Operators
*/
% connectives we take to be primitives

:- op(400,fy,nt).    %negation in t lattice
:- op(400,fy,nf).    %negation in f lattice
:- op(400,fy,ni).    %negation in i lattice

:- op(500,xfy,at).   %conjunction in t lattice
:- op(500,xfy,af).   %conjunction in f lattice
:- op(500,xfy,ai).   %conjunction in i lattice
  
:- op(600,xfy,ot).   %disjunction in t lattice
:- op(600,xfy,of).   %disjunction in f lattice
:- op(600,xfy,oi).   %disjunction in i lattice

% connectives defined from the primitives

:- op(400,fy,neg).   %Odintsov's classical negation
:- op(650,xfy,it).   %Odintsov's t implication
:- op(650,xfy,if).   %Odintsov's f implication
:- op(650,xfy,ii).   %an analogous i implication

/*
Definitions of the defined connectives (roll your own).
define(Definiendum,Definiens) will allow Definiendum to
be rewritten as Definiens.
*/

define(neg F,nt nf ni F).
define(F1 it F2,neg F1 ot F2).
define(F1 if F2,neg F1 of F2).
define(F1 ii F2,neg F1 oi F2).

/* 
The calculus is based on eight signs, which we represent here as
`t1', `f1', `n1', `b1', `t0', `f0', `n0', 
and `b0'. The predicate opposite/2 defines an obvious notion
of incompatibility. Branches close if they contain signed formulas
S1:F and S2:F, with S1 and S2 opposite signs.
*/

opposite(t1,t0).
opposite(t0,t1).
opposite(f1,f0).
opposite(f0,f1).
opposite(n1,n0).
opposite(n0,n1).
opposite(b1,b0).
opposite(b0,b1).

/* 
Next we give the predicate tableau/4, which is the heart of the
program. tableau(Signedformulas,Atoms,S,Trees) develops a tableau from
a tableau branch containing the signed formulas in Signedformulas
and the signed atoms in Atoms. If a model is found it will be described 
(in the form of a list of signed atoms). If no model is found the set
of formulas in Signedformulas + Atoms is inconsistent. The S argument 
contains a sign, while the Trees argument is used to build a graphical 
representation of the tableau. It is a list of (one or two) terms that
each represent a subtree of the tableau directly dominated by the root.

There will be rules for primitive connectives, for defined connectives, 
for closure, and for writing out sets of signed atoms.

Rules of the first kind take the first element of the Signedformulas list 
and decompose it according to the tableau expansion rules. Bottom
formulas of a rule are added as roots to subtrees of the term
under construction.
*/

/*
Negation rules
(Side conditions follow.)
*/

tableau([Sign:nt F|Rest],Atoms,S,[Tree]) :-
    ntcond(Sign,Sign1), !, 
    tableau([Sign1:F|Rest],Atoms,S,Subtrees),
    addroot(Sign1:F,Subtrees,Tree).
tableau([Sign:nf F|Rest],Atoms,S,[Tree]) :-
    nfcond(Sign,Sign1), !, 
    tableau([Sign1:F|Rest],Atoms,S,Subtrees),
    addroot(Sign1:F,Subtrees,Tree).
tableau([Sign:ni F|Rest],Atoms,S,[Tree]) :-
    nicond(Sign,Sign1), !, 
    tableau([Sign1:F|Rest],Atoms,S,Subtrees),
    addroot(Sign1:F,Subtrees,Tree).

/*
Conjunction rules
*/
tableau([Sign:(F1 at F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n0,f0,t1,b1]), !, 
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 at F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n1,f1,t0,b0]), !, 
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).
  
tableau([Sign:(F1 af F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n1,f0,t1,b0]), !, 
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 af F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n0,f1,t0,b1]), !, 
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).
  
tableau([Sign:(F1 ai F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n1,f1,t1,b1]), !,
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 ai F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n0,f0,t0,b0]), !,
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).
  
/*
Disjunction rules
*/	
tableau([Sign:(F1 ot F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n1,f1,t0,b0]), !,
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 ot F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n0,f0,t1,b1]), !,
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).
  
tableau([Sign:(F1 of F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n0,f1,t0,b1]), !,
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 of F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n1,f0,t1,b0]), !,
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).
  
tableau([Sign:(F1 oi F2)|Rest],Atoms,S,[Tree]) :-
    member(Sign,[n0,f0,t0,b0]), !,
    tableau([Sign:F1,Sign:F2|Rest],Atoms,S,Subtrees),
    addroot(Sign:F2,Subtrees,Tree1),
    addroot(Sign:F1,[Tree1],Tree).
tableau([Sign:(F1 oi F2)|Rest],Atoms,S,[Tree1,Tree2]) :-
    member(Sign,[n1,f1,t1,b1]), !,
    tableau([Sign:F1|Rest],Atoms,S,Subtrees1),
    tableau([Sign:F2|Rest],Atoms,S,Subtrees2),
    addroot(Sign:F1,Subtrees1,Tree1),
    addroot(Sign:F2,Subtrees2,Tree2).

/*
Rule for defined connectives
*/
  
tableau([Sign:F|Rest],Atoms,S,[Tree]) :-
    define(F,F1), !, 
    tableau([Sign:F1|Rest],Atoms,S,Subtrees),
    addroot(Sign:F1,Subtrees,Tree).
    
        
/* 
Closure rule
At this point any first element of the Signedformulas list is
assured to be a signed atom. If its opposite is on the Atoms
list we can close the branch.
*/

tableau([Sign:Atom|_],Atoms,_,[x]) :-
    opposite(Sign,Sign1), 
    member(Sign1:Atom,Atoms),!.

/*
Otherwise, we add the signed atom to the list of atoms already
found and continue.
*/

tableau([Sign:Atom|Rest],Atoms,S,Trees) :- !,
    tableau(Rest,[Sign:Atom|Atoms],S,Trees).

/*
If all signed formulas have been reduced to signed atoms and there
is no conflicting pair of signed atoms, we have a model, which is
a counterexample if we are testing for validity. 
*/

tableau([],Atoms,S,[o]) :- !,
    write('counterexample:'), nl,
    write(Atoms), nl, write('no transmission of '),
    write(S), nl, nl.

/* 
Side conditions on the negation rules 
*/

ntcond(n1,t1).
ntcond(t1,n1).
ntcond(f1,b1).
ntcond(b1,f1).
ntcond(n0,t0).
ntcond(t0,n0).
ntcond(f0,b0).
ntcond(b0,f0).

nfcond(n1,f1).
nfcond(f1,n1).
nfcond(t1,b1).
nfcond(b1,t1).
nfcond(n0,f0).
nfcond(f0,n0).
nfcond(t0,b0).
nfcond(b0,t0).
  
nicond(n1,b0).
nicond(b0,n1).
nicond(f1,t0).
nicond(t0,f1).
nicond(n0,b1).
nicond(b1,n0).
nicond(f0,t1).
nicond(t1,f0).

/* 
Entailment predicates, equivalence, and theorems.
*/

entailsaux(Sign, Premises, Conclusions,Tree) :-
    sign(Premises,Conclusions,Sign,SignedFormulas), !,
    tableau(SignedFormulas,[],Sign,Trees),
    initialbranch(SignedFormulas,Trees,[Tree]).
      
entailst(Premises, Conclusions,Tree1,Tree2,Tree3,Tree4) :-
    entailsaux(t1, Premises, Conclusions,Tree1),
    entailsaux(b1, Premises, Conclusions,Tree2),
    entailsaux(f0, Premises, Conclusions,Tree3),
    entailsaux(n0, Premises, Conclusions,Tree4).
	
entailsf(Premises, Conclusions,Tree1,Tree2,Tree3,Tree4) :-
    entailsaux(t1, Premises, Conclusions,Tree1),
    entailsaux(b0, Premises, Conclusions,Tree2),
    entailsaux(f0, Premises, Conclusions,Tree3),
    entailsaux(n1, Premises, Conclusions,Tree4).
	
entailsi(Premises, Conclusions,Tree1,Tree2,Tree3,Tree4) :-
    entailsaux(t1, Premises, Conclusions,Tree1),
    entailsaux(b1, Premises, Conclusions,Tree2),
    entailsaux(f1, Premises, Conclusions,Tree3),
    entailsaux(n1, Premises, Conclusions,Tree4).

entails(Premises, Conclusions,Tree1,Tree2,Tree3,Tree4,Tree5,Tree6) :-
    entailsaux(t1, Premises, Conclusions,Tree1),
    entailsaux(b1, Premises, Conclusions,Tree2),
    entailsaux(b0, Premises, Conclusions,Tree3),
    entailsaux(f0, Premises, Conclusions,Tree4),
    entailsaux(n1, Premises, Conclusions,Tree5),
    entailsaux(n0, Premises, Conclusions,Tree6).
  
equiv(Formula1,Formula2,Tree1,Tree2,Tree3,Tree4,Tree5,Tree6,Tree7,Tree8) :-
    entailsaux(t1, [Formula1], [Formula2],Tree1),
    entailsaux(b1, [Formula1], [Formula2],Tree2),
    entailsaux(f1, [Formula1], [Formula2],Tree3),
    entailsaux(n1, [Formula1], [Formula2],Tree4),
    entailsaux(t0, [Formula1], [Formula2],Tree5),
    entailsaux(b0, [Formula1], [Formula2],Tree6),
    entailsaux(f0, [Formula1], [Formula2],Tree7),
    entailsaux(n0, [Formula1], [Formula2],Tree8).

thmt(Formula,Tree1,Tree2,Tree3,Tree4) :- 
    entailst([],[Formula],Tree1,Tree2,Tree3,Tree4).
thmf(Formula,Tree1,Tree2,Tree3,Tree4) :- 
    entailsf([],[Formula],Tree1,Tree2,Tree3,Tree4).
thmi(Formula,Tree1,Tree2,Tree3,Tree4) :- 
    entailsi([],[Formula],Tree1,Tree2,Tree3,Tree4).
thm(Formula,Tree1,Tree2,Tree3,Tree4,Tree5,Tree6) :- 
    entails([],[Formula],Tree1,Tree2,Tree3,Tree4,Tree5,Tree6).

/*
Some predicates to do with the term representation of the
tree. addroot/3 takes a collection of trees (terms) and
adds a root (functor), so that the result is a single tree.
initialbranch/3 uses this to provide a collection of trees
with a common initial branch.
*/

addroot(Signedformula,Trees,Tree) :-
    term_to_atom(Signedformula,Quoted),
    Tree =.. [Quoted|Trees].
  
initialbranch([],Trees,Trees).
  
initialbranch([Signedformula|Rest],Trees,[Tree]) :-
    initialbranch(Rest,Trees,Trees1),
    addroot(Signedformula,Trees1,Tree).

/*
sign(Premises, Conclusions, Sign, SignedFormulas) signs
the formulas in Premises with Sign and those in Conclusions 
with its opposite. The signed formulas are collected in 
SignedFormulas.
*/

sign([],[],_,[]).
sign([],[F|Rest],Sign,[Sign2:F|SignedRest]) :-
    opposite(Sign,Sign2), sign([],Rest,Sign,SignedRest).
sign([F|Rest],Conclusions,Sign,[Sign:F|SignedRest]) :-
    sign(Rest,Conclusions,Sign,SignedRest).

/** <examples>
Some valid, some not.
?- entails([p at q],[p ot q],Tree1,Tree2,Tree3,Tree4,Tree5,Tree6).
?- entailst([p at q],[p ot q],Tree1,Tree2,Tree3,Tree4).
?- entails([p at q],[p],Tree1,Tree2,Tree3,Tree4,Tree5,Tree6).
?- entailst([p at q],[p],Tree1,Tree2,Tree3,Tree4).
?- entails([p at q],[p of q],Tree1,Tree2,Tree3,Tree4,Tree5,Tree6).
?- entailst([p, p it q],[q],Tree1,Tree2,Tree3,Tree4).
?- equiv(p at (q of r oi s),(p at q) of (p at r) oi (p at s),Tree1,Tree2,Tree3,Tree4,Tree5,Tree6,Tree7,Tree8).
?- equiv(p at q af r ai s,s at r af q ai p,Tree1,Tree2,Tree3,Tree4,Tree5,Tree6,Tree7,Tree8).
?- equiv(neg (p at q af r ai s),neg p ot neg q of neg r oi neg s,Tree1,Tree2,Tree3,Tree4,Tree5,Tree6,Tree7,Tree8).
?- equiv(nf (p at (q af (r ai s))),nf p at (nf q of (nf r ai nf s)),Tree1,Tree2,Tree3,Tree4,Tree5,Tree6,Tree7,Tree8).
?- thmt((p it (q it r)) it ((p it q) it (p it r)),Tree1,Tree2,Tree3,Tree4).
?- thm((p it (q it r)) it ((p it q) it (p it r)),Tree1,Tree2,Tree3,Tree4,Tree5,Tree6).
*/