/*
Copyright 2020 Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato.
This file is part of HYPNO. HYPNO is free software: you can redistribute it and/or modify it under
the terms of the GNU General Public License as published by the Free Software Foundation, either version
3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will
be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy
of the GNU General Public License along with HYPNO. If not, see .
*/
/* imports */
:- use_module(library(lists)).
:- op(800,fy,-),
op(700,fy,box),
op(680,xfy,=>),
op(650,xfy,->),
op(600,xfy,^),
op(600,xfy,?).
/* Top level predicates for launching the theorem prover */
prove(Formula):-
terminating_proof_search([singleSeq([[],[Formula]],[])],Tree),write(Tree),!.
% In case of failure, the application builds a counter model from an open saturated branch
prove(_):-write('COUNTER').
counter(Formula):-
write('COUNTER'),
build_saturated_branch([singleSeq([[],[Formula]],[])],model(PrintableHyper)),
partitionPrintable(PrintableHyper,Sigma,Delta),
extractWorlds(Sigma,ListOfWorlds),
write('
'),
write('W = {'),
writeListOfWorlds(ListOfWorlds),
write('} | | '),
length(ListOfWorlds,N),
extractEval(Sigma,N,PropEval),
evalPropVars(PropEval,ByPropVars),
writeBetterPropVars(ByPropVars),
write(' |
'),
extractBlocks(Sigma,Sigma,Delta,N,SigmaPlus,SigmaMinus),
extractEvalSigmas(Sigma,N,SigmaPlus,SigmaMinus,Nonmon,Monot),
write('N (monotonic case):
'),
writeBetter(Monot),
% write('N (non-monotonic case):
'),
% writeBetter(Nonmon),
write('
').
/* Auxiliary predicate implementing the calculi */
% Axioms
terminating_proof_search(Hyper,tree(axiom,PrintableHyper,no,no)):-
member(singleSeq([Gamma,Delta],_),Hyper),
member(P,Gamma),
member(P,Delta),
!,
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(axf,PrintableHyper,no,no)):-
member(singleSeq([Gamma,_],_),Hyper),
member(false,Gamma),
!,
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(axt,PrintableHyper,no,no)):-
member(singleSeq([_,Delta],_),Hyper),
member(true,Delta),
!,
extractPrintableSequents(Hyper,PrintableHyper).
% []L
terminating_proof_search(Hyper,tree(lbox,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(box A,Gamma),
\+member(box A,Additional),
!,
terminating_proof_search([singleSeq([[[A]|Gamma],Delta],[box A|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
% Rule C
terminating_proof_search(Hyper,tree(c,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(Sigma,Gamma),
is_list(Sigma),
member(Pi,Gamma),
is_list(Pi),
list_to_ord_set(Sigma,SigmaOrd),
list_to_ord_set(Pi,PiOrd),
\+ord_symdiff(Sigma,Pi,[]),
\+member(c(SigmaOrd,PiOrd),Additional),
\+member(c(PiOrd,SigmaOrd),Additional),
append(Sigma,Pi,NewBlock),
list_to_ord_set(NewBlock,NewOrd),
\+member(NewOrd,Gamma),
!,
terminating_proof_search([singleSeq([[NewOrd|Gamma],Delta],[c(PiOrd,SigmaOrd)|[c(SigmaOrd,PiOrd)|Additional]])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
% M[]R
terminating_proof_search(Hyper,tree(mrbox,PrintableHyper,Sub1,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(Sigma,Gamma),
is_list(Sigma),
member(box B,Delta),
list_to_ord_set(Sigma,SigmaOrd),
\+member(apdR(SigmaOrd,B),Additional),
!,
terminating_proof_search([singleSeq([Sigma,[B]],[])|[singleSeq([Gamma,Delta],[apdR(SigmaOrd,B)|Additional])|NewHyper]],Sub1),
extractPrintableSequents(Hyper,PrintableHyper).
% Rules for boolean connectives
terminating_proof_search(Hyper,tree(andL,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ^ B,Gamma),
\+member(left(A ^ B),Additional),
!,
terminating_proof_search([singleSeq([[A|[B|Gamma]],Delta],[left(A ^ B)|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(orR,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ? B,Delta),
\+member(right(A ? B),Additional),
!,
terminating_proof_search([singleSeq([Gamma,[A|[B|Delta]]],[right(A ? B)|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(notL,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(-A,Gamma),
\+member(left(-A),Additional),
!,
terminating_proof_search([singleSeq([Gamma,[A|Delta]],[left(-A)|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(notR,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(-A,Delta),
\+member(right(-A),Additional),
!,
terminating_proof_search([singleSeq([[A|Gamma],Delta],[right(-A)|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(impR,PrintableHyper,SubTree,no)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A -> B,Delta),
\+member(right(A -> B),Additional),
!,
terminating_proof_search([singleSeq([[A|Gamma],[B|Delta]],[right(A -> B)|Additional])|NewHyper],SubTree),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(andR,PrintableHyper,Sub1,Sub2)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ^ B,Delta),
\+member(right(A ^ B),Additional),
!,
terminating_proof_search([singleSeq([Gamma,[A|Delta]],[right(A ^ B)|Additional])|NewHyper],Sub1),
terminating_proof_search([singleSeq([Gamma,[B|Delta]],[right(A ^ B)|Additional])|NewHyper],Sub2),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(orL,PrintableHyper,Sub1,Sub2)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ? B,Gamma),
\+member(left(A ? B),Additional),
!,
terminating_proof_search([singleSeq([[A|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Sub1),
terminating_proof_search([singleSeq([[B|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Sub2),
extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(impL,PrintableHyper,Sub1,Sub2)):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A -> B,Gamma),
\+member(left(A -> B),Additional),
!,
terminating_proof_search([singleSeq([Gamma,[A|Delta]],[left(A -> B)|Additional])|NewHyper],Sub1),
terminating_proof_search([singleSeq([[B|Gamma],Delta],[left(A -> B)|Additional])|NewHyper],Sub2),
extractPrintableSequents(Hyper,PrintableHyper).
% Predicate checking whether a sequent is an instance of an axiom
instanceOfAnAxiom(Hyper):-
member(singleSeq([Gamma,Delta],_),Hyper),
member(P,Gamma),
member(P,Delta),
!.
instanceOfAnAxiom(Hyper):-
member(singleSeq([Gamma,_],_),Hyper),
member(false,Gamma),
!.
instanceOfAnAxiom(Hyper):-
member(singleSeq([_,Delta],_),Hyper),
member(true,Delta),!.
/* Auxiliary predicate implementing the construction of a countermodel */
% []L
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(box A,Gamma),
\+member(box A,Additional),
!,
build_saturated_branch([singleSeq([[[A]|Gamma],Delta],[box A|Additional])|NewHyper],Model).
% C
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(Sigma,Gamma),
is_list(Sigma),
member(Pi,Gamma),
is_list(Pi),
list_to_ord_set(Sigma,SigmaOrd),
list_to_ord_set(Pi,PiOrd),
\+member(c(SigmaOrd,PiOrd),Additional),
\+member(c(PiOrd,SigmaOrd),Additional),
append(Sigma,Pi,NewBlock),
list_to_ord_set(NewBlock,NewOrd),
\+member(NewOrd,Gamma),
build_saturated_branch([singleSeq([[NewOrd|Gamma],Delta],[c(PiOrd,SigmaOrd)|[c(SigmaOrd,PiOrd)|Additional]])|NewHyper],Model).
% M[]R
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(Sigma,Gamma),
is_list(Sigma),
member(box B,Delta),
list_to_ord_set(Sigma,SigmaOrd),
\+member(apdR(SigmaOrd,B),Additional),
build_saturated_branch([singleSeq([Sigma,[B]],[])|[singleSeq([Gamma,Delta],[apdR(SigmaOrd,B)|Additional])|NewHyper]],Model).
% Rules for boolean connectives
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ^ B,Gamma),
\+member(left(A ^ B),Additional),
!,
build_saturated_branch([singleSeq([[A|[B|Gamma]],Delta],[left(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ? B,Delta),
\+member(right(A ? B),Additional),
!,
build_saturated_branch([singleSeq([Gamma,[A|[B|Delta]]],[right(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(-A,Gamma),
\+member(left(-A),Additional),
!,
build_saturated_branch([singleSeq([Gamma,[A|Delta]],[left(-A)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(-A,Delta),
\+member(right(-A),Additional),
!,
build_saturated_branch([singleSeq([[A|Gamma],Delta],[right(-A)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A -> B,Delta),
\+member(right(A -> B),Additional),
!,
build_saturated_branch([singleSeq([[A|Gamma],[B|Delta]],[right(A -> B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ^ B,Delta),
\+member(right(A ^ B),Additional),
build_saturated_branch([singleSeq([Gamma,[A|Delta]],[right(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ^ B,Delta),
\+member(right(A ^ B),Additional),
build_saturated_branch([singleSeq([Gamma,[B|Delta]],[right(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ? B,Gamma),
\+member(left(A ? B),Additional),
build_saturated_branch([singleSeq([[A|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A ? B,Gamma),
\+member(left(A ? B),Additional),
build_saturated_branch([singleSeq([[B|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A -> B,Gamma),
\+member(left(A -> B),Additional),
build_saturated_branch([singleSeq([Gamma,[A|Delta]],[left(A -> B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
member(A -> B,Gamma),
\+member(left(A -> B),Additional),
build_saturated_branch([singleSeq([[B|Gamma],Delta],[left(A -> B)|Additional])|NewHyper],Model).
% If no further rule is applicable and the branch is not closed, we have found a closed saturated branch and we are done
build_saturated_branch(Hyper,model(Hyper)):-
true,
\+instanceOfAnAxiom(Hyper).
% extractPrintableSequents(Hyper,PrintableHyper),
% Auxiliary predicates for building the countermodel and showing it by means of the graphical interface
extractPrintableSequents([],[]):-!.
extractPrintableSequents([singleSeq([Sigma,Delta],_)|Tail],[[Sigma,Delta]|PrintTail]):-
!,
extractPrintableSequents(Tail,PrintTail).
writeBetterPropVars([]):-!,write(' For all atomic variables P, V(P)=∅').
writeBetterPropVars([[P,[]]]):-
write('V('),write(P),write(')=∅'),write('
For all other atomic variables P (if any), V(P)=∅').
writeBetterPropVars([[P,[]]|Tail]):-
write('V('),write(P),write(')=∅, '),writeBetterPropVars(Tail).
writeBetterPropVars([[P,ListOfWorlds]]):-
write('V('),write(P),write(')={'),writeListOfWorlds(ListOfWorlds),write('}'),write('
For all other atomic variables P (if any), V(P)=∅').
writeBetterPropVars([[P,ListOfWorlds]|Tail]):-
write('V('),write(P),write(')={'),writeListOfWorlds(ListOfWorlds),
write('}, '),writeBetterPropVars(Tail).
evalPropVars(PropEval,ByPropVars):-
listOfAtomicFormulas(PropEval,Atoms),
whereAtomIsTrue(Atoms,PropEval,ByPropVars).
whereAtomIsTrue([],_,[]):-!.
whereAtomIsTrue([P|OtherAtoms],PropEval,[[P,ListOfWorlds]|RestOfAtoms]):-
findall(W,(member([W,WEval],PropEval),member(P,WEval)),ListOfWorlds),
whereAtomIsTrue(OtherAtoms,PropEval,RestOfAtoms).
listOfAtomicFormulas([],[]):-!.
listOfAtomicFormulas([[_,ListOfFormulas]|Tail],DefAtoms):-
listOfAtoms(ListOfFormulas,Atoms),
listOfAtomicFormulas(Tail,ResTail),
list_to_ord_set(Atoms,A1),
list_to_ord_set(ResTail,A2),
ord_union(A1,A2,DefAtoms).
listOfAtoms([],[]):-!.
listOfAtoms([true|Tail],ResTail):-!,listOfAtoms(Tail,ResTail).
listOfAtoms([false|Tail],ResTail):-!,listOfAtoms(Tail,ResTail).
listOfAtoms([Fml|Tail],[Fml|ResTail]):-atom(Fml),!,listOfAtoms(Tail,ResTail).
listOfAtoms([_|Tail],ResTail):-listOfAtoms(Tail,ResTail).
writeListOfWorlds([W]):-write(W),!.
writeListOfWorlds([W|Tail]):-write(W),write(', '),writeListOfWorlds(Tail).
writeFormulas([]):-!.
writeFormulas([Fml]):-!,write(Fml).
writeFormulas([Fml|Tail]):-write(Fml),write(', '),writeFormulas(Tail).
writeBetter([]):-!.
writeBetter([(N,[])|Tail]):-
write('N('),write(N),write(')=∅
'),
writeBetter(Tail).
writeBetter([(N,List)|Tail]):-
write('N('),write(N),write(')={'),
writeList(List),
write('}
'),
writeBetter(Tail).
writeList([(Plus,Minus)]):-!,
write('('),
write(Plus),
write(','),
write(Minus),
write(')').
writeList([(Plus,Minus)|Tail]):-!,
write('('),
write(Plus),
write(','),
write(Minus),
write('),'),
writeList(Tail).
extractEvalSigmas([],_,_,_,[],[]):-!.
extractEvalSigmas([Hyper|Tail],N,SigmaPlus,SigmaMinus,[(N,MonotBlock)|MonotOthers],[(N,NonmonBlock)|NonmonOthers]):-
valBlocks(Hyper,N,SigmaPlus,SigmaMinus,MonotBlock,NonmonBlock),
N1 is N-1,
extractEvalSigmas(Tail,N1,SigmaPlus,SigmaMinus,MonotOthers,NonmonOthers).
valBlocks([],_,_,_,[],[]):-!.
valBlocks([Block|Tail],N,SigmaPlus,SigmaMinus,[(SP,SM)|Monot],[(SP,[])|Nonmon]):-
is_list(Block),
!,
flatten(SigmaPlus,FlatSP),
flatten(SigmaMinus,FlatSM),
member(plus(Block,SP),FlatSP),
member(minus(Block,SM),FlatSM),
valBlocks(Tail,N,SigmaPlus,SigmaMinus,Monot,Nonmon).
valBlocks([_|Tail],N,SigmaPlus,SigmaMinus,Monot,Nonmon):-
valBlocks(Tail,N,SigmaPlus,SigmaMinus,Monot,Nonmon).
extractBlocks([],_,_,_,[],[]):-!.
extractBlocks([Hyper|Tail],Sigma,Delta,N,[HyperPlus|TailPlus],[HyperMinus|TailMinus]):-
forEachBlock(Hyper,Sigma,Delta,N,HyperPlus,HyperMinus),
extractBlocks(Tail,Sigma,Delta,N,TailPlus,TailMinus).
forEachBlock([],_,_,_,[],[]):-!.
forEachBlock([Block|Tail],Sigma,Delta,N,[plus(Block,BlockPlus)|TailPlus],[minus(Block,BlockMinus)|TailMinus]):-
is_list(Block),!,
blockSetPlus(Block,Sigma,N,BlockPlus),
blockSetMinus(Block,Delta,N,BlockMinus),
forEachBlock(Tail,Sigma,Delta,N,TailPlus,TailMinus).
forEachBlock([_|Tail],Sigma,Delta,N,TailPlus,TailMinus):-
forEachBlock(Tail,Sigma,Delta,N,TailPlus,TailMinus).
partitionPrintable([],[],[]):-!.
partitionPrintable([singleSeq([Sigma,Delta],_)|Tail],[Sigma|SigmaTail],[Delta|DeltaTail]):-
partitionPrintable(Tail,SigmaTail,DeltaTail).
% blockSetPlus(Block,Model,N,SigmaPlus)
blockSetPlus(_,_,0,[]):-!.
blockSetPlus(Block,[Hyper|Rest],N,[N|Others]):-
list_to_ord_set(Block,SetSigma),
list_to_ord_set(Hyper,SetHyper),
ord_subset(SetSigma,SetHyper),
!,
N1 is N-1,
blockSetPlus(Block,Rest,N1,Others).
blockSetPlus(Block,[_|Rest],N,Others):-
N1 is N-1,
blockSetPlus(Block,Rest,N1,Others).
% blockSetMinus(Block,Model,N,SigmaMinus)
blockSetMinus(_,_,0,[]):-!.
blockSetMinus(Block,[Hyper|Rest],N,Others):-
intersection(Block,Hyper,[]),
!,
N1 is N-1,
blockSetMinus(Block,Rest,N1,Others).
blockSetMinus(Block,[_|Rest],N,[N|Others]):-
N1 is N-1,
blockSetMinus(Block,Rest,N1,Others).
extractEval([],_,[]):-!.
extractEval([SatSeq|Tail],N,[[N,PropEvalCurSatSeq]|PropEvalOthers]):-
auxPropEval(SatSeq,PropEvalCurSatSeq),
N1 is N-1,
extractEval(Tail,N1,PropEvalOthers).
auxPropEval([],[]):-!.
auxPropEval([List|Tail],PropEvalTail):-is_list(List),!,auxPropEval(Tail,PropEvalTail).
auxPropEval([Head|Tail],[Head|ResTail]):-auxPropEval(Tail,ResTail).
extractWorlds(Hyper,ListOfWorlds):-length(Hyper,N),buildWorlds(N,ListOfWorlds).
buildWorlds(0,[]):-!.
buildWorlds(N,[N|Tail]):-N1 is N-1,buildWorlds(N1,Tail).
/* Remove duplicates in a list */
remove_duplicates([],[]):-!.
remove_duplicates([X|Tail],ResTail):-member(X,Tail),!,remove_duplicates(Tail,ResTail).
remove_duplicates([X|Tail],[X|ResTail]):-remove_duplicates(Tail,ResTail).
/* Auxiliary predicates for building the latex source file containing a derivation of a sequent */
getRuleName(tree(axiom,_,_,_)):-write('\\mbox{\\bf init}'),!.
getRuleName(tree(axt,_,_,_)):-write('\\top_R'),!.
getRuleName(tree(axf,_,_,_)):-write('\\bot_L'),!.
getRuleName(tree(notR,_,_,_)):-write('\\lnot_R'),!.
getRuleName(tree(notL,_,_,_)):-write('\\lnot_L'),!.
getRuleName(tree(orR,_,_,_)):-write('\\vee_R'),!.
getRuleName(tree(orL,_,_,_)):-write('\\vee_L'),!.
getRuleName(tree(n,_,_,_)):-write('N'),!.
getRuleName(tree(c,_,_,_)):-write('C'),!.
getRuleName(tree(m,_,_,_)):-write('M'),!.
getRuleName(tree(prv,_,_,_)):-write('E\\Rrightarrow'),!.
getRuleName(tree(andR,_,_,_)):-write('\\land_R'),!.
getRuleName(tree(andL,_,_,_)):-write('\\land_L'),!.
getRuleName(tree(impL,_,_,_)):-write('\\rightarrow_L'),!.
getRuleName(tree(impR,_,_,_)):-write('\\rightarrow_R'),!.
getRuleName(tree(lbox,_,_,_)):-write('\\square_L'),!.
getRuleName(tree(rbox,_,_,_)):-write('\\square_R'),!.
getRuleName(tree(mrbox,_,_,_)):-write('M\\square_R'),!.
getFirstSon(tree(_,_,SubTree,_)):-write(SubTree),!.
getSecondSon(tree(_,_,_, SubTree)):-write(SubTree),!.
getNode(tree(_,HyperSequent,_,_)):-
listAllHyper(HyperSequent),!.
listAllHyper([[Sigma,Delta]]):-
listAllFmls(Sigma),
write(' \\Rightarrow '),
listAllFmls(Delta).
listAllHyper([[Sigma,Delta]|OtherSeqs]):-
listAllFmls(Sigma),
write(' \\Rightarrow '),
listAllFmls(Delta),
write(' \\ \\mid \\ '),
listAllHyper(OtherSeqs).
listAllFmls([]):-!.
listAllFmls([Fml]):-
is_list(Fml),!,
write('\\langle '),
listAllFmls(Fml),
write('\\rangle ').
listAllFmls([Fml]):-
betterFormula(Fml).
listAllFmls([Fml|Tail]):-
is_list(Fml),!,
write('\\langle '),
listAllFmls(Fml),
write('\\rangle, '),
listAllFmls(Tail).
listAllFmls([Fml|Tail]):-
betterFormula(Fml),
write(','),
listAllFmls(Tail).
betterFormula(false):-!,write('\\bot').
betterFormula(true):-!,write('\\top').
betterFormula(-A):-!,write('\\lnot ('),betterFormula(A),write(')').
betterFormula(A ^ B):-!,betterFormula(A),write(' \\land '),betterFormula(B).
betterFormula(A ? B):-!,betterFormula(A),write(' \\vee '),betterFormula(B).
betterFormula(A -> B):-!,betterFormula(A),write(' \\rightarrow '),betterFormula(B).
betterFormula(A => B):-!,betterFormula(A),write(' E\\Rrightarrow '),betterFormula(B).
betterFormula(box A):-!,write(' \\square( '),betterFormula(A),write(')').
betterFormula(P):-write(P).
printAtomicFormulas([]):-!,write("").
printAtomicFormulas([true]):-!,write("").
printAtomicFormulas([true|Tail]):-!,write(", "),printAtomicFormulas(Tail).
printAtomicFormulas([A]):-!,write(A).
printAtomicFormulas([A|Tail]):-write(A),write(", "),printAtomicFormulas(Tail).
printOnWebPage([]):-!,write('').
printOnWebPage([X]):-!,write(X).
printOnWebPage([X|Tail]):-write(X),write(', '),printOnWebPage(Tail).