/*
Copyright 2019 Tiziano Dalmonte, Sara Negri, Nicola Olivetti, Gian Luca Pozzato.
This file is part of PRONOM. PRONOM 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 PRONOM. If not, see .
*/
/* imports */
:- use_module(library(lists)).
:- include("operators.pl").
:- include("common.pl").
/* Top level predicates for launching the theorem prover */
prove(Formula):-
generate_empty_spheres([x],InitialSpheres),
terminating_proof_search(InitialSpheres,[],[[x,Formula]],Tree,[],[],[]),write(Tree),!.
% In case of failure, the application builds a counter model from an open saturated branch
prove(Formula):-write('COUNTER'),
generate_empty_spheres([x],InitialSpheres),
build_saturate_branch(InitialSpheres,[],[[x,Formula]],model(Spheres,Gamma,Delta),[],[],[]),
completeDec(Spheres,TempSpheres),
removeUseless(TempSpheres,NewSpheres),
getIntegrationCounterModel(Spheres,Gamma,AdditionalDefinitions),
append(NewSpheres,AdditionalDefinitions,DefSpheres),
write(model(DefSpheres,Gamma,Delta)).
% Predicates to apply dec
completeDec(Spheres,NewSpheres):-
findall(X,(member([X,[comb(_)|_]],Spheres)),List),
cDecAux(List,Spheres,NewSpheres).
cDecAux([],_,[]):-!.
cDecAux([X|Tail],Spheres,[[X,NewSphOfX]|TailSpheres]):-!,
select([X,[comb(List)|OtherX]],Spheres,TempSpheres),
powerset(List,Pow),
addX(Pow,X,XPow),
flatten(XPow,OKPow),
append([comb(List)|OtherX],OKPow,TempX),
remove_duplicates(TempX,NewSphOfX),
cDecAux(Tail,TempSpheres,TailSpheres).
addX([],_,[]):-!.
addX([S|Tail],X,[S|ResTail]):-length(S,1),!,addX(Tail,X,ResTail).
addX([S|Tail],X,[comb(S)|ResTail]):-addX(Tail,X,ResTail).
%powerset(X,Y) :- bagof(S,subseq(S,X),Y).
subseq([],[]).
subseq([],[_|_]).
subseq([X|Xs],[X|Ys]):-subseq(Xs,Ys).
subseq([X|Xs],[_|Ys]):-append(_,[X|Zs],Ys),subseq(Xs,Zs).
removeUseless([],[]):-!.
removeUseless([[X,List]|Tail],[[X,NewList]|ResTail]):-
removeEmptyComb(List,NewList),
removeUseless(Tail,ResTail).
removeEmptyComb([],[]):-!.
removeEmptyComb([comb([])|Tail],Tail):-!.
removeEmptyComb([Head|Tail],[Head|ResTail]):-removeEmptyComb(Tail,ResTail).
getIntegrationCounterModel([],_,[]):-!.
getIntegrationCounterModel([[_,SpOfX]|Tail],Gamma,[[uns(List),AdditionalDefsUns]|[[bar(List),AdditionalDefsBar]|ResTail]]):-
member(comb(List),SpOfX),!,
integrateUnsigned(List,Gamma,AdditionalDefsUns),
integrateBar(List,Gamma,AdditionalDefsBar),
getIntegrationCounterModel(Tail,Gamma,ResTail).
getIntegrationCounterModel([_|Tail],Gamma,ResTail):-
getIntegrationCounterModel(Tail,Gamma,ResTail).
integrateUnsigned(_,[],[]):-!.
integrateUnsigned(List,[[_,0,X]|Tail],[X|ResTail]):-
forEachElement(List,X,[[_,0,X]|Tail]),!,
integrateUnsigned(List,Tail,ResTail).
integrateUnsigned(List,[_|Tail],ResTail):-!,
integrateUnsigned(List,Tail,ResTail).
forEachElement([],_,_):-!.
forEachElement([T|Tail],X,Gamma):-member([T,0,X],Gamma),forEachElement(Tail,X,Gamma).
integrateBar(List,Gamma,ListOfAdditionalInformation):-
findall(X,partOfBar(X,List,Gamma),ListOfAdditionalInformation).
partOfBar(X,List,Gamma):-member([T,1,X],Gamma),member(T,List).
printAdditional([]):-!,write("").
printAdditional([[uns(List),[]]]):-!,
write("["),
printList(List),
write("]=∅").
printAdditional([[uns(List),[]]|Tail]):-!,
write("["),
printList(List),
write("]=∅"),
write(", "),
printAdditional(Tail).
printAdditional([[bar(List),[]]]):-!,
write("["),
printList(List),
write("]=∅").
printAdditional([[bar(List),[]]|Tail]):-!,
write("["),
printList(List),
write("]=∅"),
write(", "),
printAdditional(Tail).
printAdditional([[uns(List),Worlds]]):-!,
write("["),
printList(List),
write("]={"),
writeBetter(Worlds),
write("}").
printAdditional([[uns(List),Worlds]|Tail]):-!,
write("["),
printList(List),
write("]={"),
writeBetter(Worlds),
write("}"),
printAdditional(Tail).
printAdditional([[bar(List),Worlds]]):-!,
write("["),
printList(List),
write("]={"),
writeBetter(Worlds),
write("}").
printAdditional([[bar(List),Worlds]|Tail]):-!,
write("["),
printList(List),
write("]={"),
writeBetter(Worlds),
write("}"),
printAdditional(Tail).
printList([]):-!,write("").
printList([T]):-!,betterNameofSphereHTML(T).
printList([T|Tail]):-betterNameofSphereHTML(T),write(", "),printList(Tail).
writeBetter([]):-!,write("").
writeBetter([W]):-!,write(W).
writeBetter([Head|Tail]):-write(Head),write(", "),writeBetter(Tail).
/* Auxiliary predicate implementing LSE calculi */
% Axioms
terminating_proof_search(Spheres,Gamma,Delta,tree(axiom,[Spheres,Gamma,Delta],no,no),_,_,_):-
member([X,A],Gamma),
member([X,A],Delta),
!.
terminating_proof_search(Spheres,Gamma,Delta,tree(axf,[Spheres,Gamma,Delta],no,no),_,_,_):-
member([_,false],Gamma),
!.
terminating_proof_search(Spheres,Gamma,Delta,tree(axt,[Spheres,Gamma,Delta],no,no),_,_,_):-
member([_,true],Delta),
!.
% Axiom N
terminating_proof_search(Spheres,Gamma,Delta,tree(nsigned,[Spheres,Gamma,Delta],no,no),_,_,_):-
member([-1,1,_],Gamma),
!.
% Rules for boolean connectives
terminating_proof_search(Spheres,Gamma,Delta,tree(notR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,-A],Delta,NewDelta),!,
terminating_proof_search(Spheres,[[X,A]|Gamma],NewDelta,SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(notL,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,-A],Gamma,NewGamma),!,
terminating_proof_search(Spheres,NewGamma,[[X,A]|Delta],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(andL,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,A ^ B],Gamma,NewGamma),!,
terminating_proof_search(Spheres,[[X,A]|[[X,B]|NewGamma]],Delta,SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(orR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,A ? B],Delta,NewDelta),!,
terminating_proof_search(Spheres,Gamma,[[X,A]|[[X,B]|NewDelta]],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(impR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,A >> B],Delta,NewDelta),!,
terminating_proof_search(Spheres,[[X,A]|Gamma],[[X,B]|NewDelta],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(andR,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
select([X,A ^ B],Delta,NewDelta),!,
terminating_proof_search(Spheres,Gamma,[[X,A]|NewDelta],Sub1,RBox,RExist,LAll),
terminating_proof_search(Spheres,Gamma,[[X,B]|NewDelta],Sub2,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(orL,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
select([X,A ? B],Gamma,NewGamma),!,
terminating_proof_search(Spheres,[[X,A]|NewGamma],Delta,Sub1,RBox,RExist,LAll),
terminating_proof_search(Spheres,[[X,B]|NewGamma],Delta,Sub2,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(impL,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
select([X,A >> B],Gamma,NewGamma),!,
terminating_proof_search(Spheres,NewGamma,[[X,A]|Delta],Sub1,RBox,RExist,LAll),
terminating_proof_search(Spheres,[[X,B]|NewGamma],Delta,Sub2,RBox,RExist,LAll).
% L[]
terminating_proof_search(Spheres,Gamma,Delta,tree(lbox,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,box A],Gamma,NewGamma),!,
select([X,SpOfX],Spheres,NewSpheres),
freshSphere(Spheres,T),
terminating_proof_search([[X,[T|SpOfX]]|NewSpheres],[[forall,T,0,A]|NewGamma],[[exists,T,1,A]|Delta],SubTree,RBox,RExist,LAll).
% N unsigned
terminating_proof_search(Spheres,Gamma,Delta,tree(nunsigned,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,SpOfX],Spheres,NewSpheres),
\+member(-1,SpOfX),!,
terminating_proof_search([[X,[-1|SpOfX]]|NewSpheres],Gamma,Delta,SubTree,RBox,RExist,LAll).
% L||-exists
terminating_proof_search(Spheres,Gamma,Delta,tree(lexists,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([exists,T,1,A],Gamma,NewGamma),!,
freshLabel(Spheres,Gamma,Delta,X),
terminating_proof_search([[X,[]]|Spheres],[[T,1,X]|[[X,A]|NewGamma]],Delta,SubTree,RBox,RExist,LAll).
% R||- forall
terminating_proof_search(Spheres,Gamma,Delta,tree(rforall,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([forall,T,0,A],Delta,NewDelta),!,
freshLabel(Spheres,Gamma,Delta,X),
terminating_proof_search([[X,[]]|Spheres],[[T,0,X]|Gamma],[[X,A]|NewDelta],SubTree,RBox,RExist,LAll).
% Rule R||-exists
% No longer needed since the optimization of R[]
/*
terminating_proof_search(Spheres,Gamma,Delta,tree(rexists,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
member([exists,T,1,A],Delta),
member([T,1,X],Gamma),
\+member([T,1,X,A],RExist),!,
terminating_proof_search(Spheres,Gamma,[[X,A]|Delta],SubTree,RBox,[[T,1,X,A]|RExist],LAll).
*/
% Rule L ||-forall
terminating_proof_search(Spheres,Gamma,Delta,tree(lforall,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
member([forall,T,0,A],Gamma),
member([T,0,X],Gamma),
\+member([T,0,X,A],LAll),!,
terminating_proof_search(Spheres,[[X,A]|Gamma],Delta,SubTree,RBox,RExist,[[T,0,X,A]|LAll]).
% Rule R[]
terminating_proof_search(Spheres,Gamma,Delta,tree(rbox,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
member([X,box A],Delta),
member([X,SpOfX],Spheres),
member(T,SpOfX),
\+member([X,A,T],RBox),!,
terminating_proof_search(Spheres,Gamma,[[forall,T,0,A]|Delta],SubTree,[[X,A,T]|RBox],RExist,LAll).
% Rule C
terminating_proof_search(Spheres,Gamma,Delta,tree(c,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
select([X,SpOfX],Spheres,TempSpheres),
SpOfX \== [],
\+member(comb(_),SpOfX),
terminating_proof_search([[X,[comb(SpOfX)|SpOfX]]|TempSpheres],Gamma,Delta,SubTree,RBox,RExist,LAll).
% Rule dec
terminating_proof_search(Spheres,Gamma,Delta,tree(dec,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
member([comb(List),0,X],Gamma),
member(T,List),
member(S,List),
T> B],Delta,NewDelta),!,
build_saturate_branch(Spheres,[[X,A]|Gamma],[[X,B]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,A ^ _],Delta,NewDelta),
build_saturate_branch(Spheres,Gamma,[[X,A]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,_ ^ B],Delta,NewDelta),
build_saturate_branch(Spheres,Gamma,[[X,B]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,A ? _],Gamma,NewGamma),
build_saturate_branch(Spheres,[[X,A]|NewGamma],Delta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,_ ? B],Gamma,NewGamma),
build_saturate_branch(Spheres,[[X,B]|NewGamma],Delta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,A >> _],Gamma,NewGamma),
build_saturate_branch(Spheres,NewGamma,[[X,A]|Delta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,_ >> B],Gamma,NewGamma),
build_saturate_branch(Spheres,[[X,B]|NewGamma],Delta,Model,RBox,RExist,LAll).
% Rule C
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
select([X,SpOfX],Spheres,TempSpheres),
SpOfX \== [],
\+member(comb(_),SpOfX),
build_saturate_branch([[X,[comb(SpOfX)|SpOfX]]|TempSpheres],Gamma,Delta,Model,RBox,RExist,LAll).
% Rule dec
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
member([comb(List),0,X],Gamma),
member(T,List),
member(S,List),
T