/* Copyright 2011 Laura Giordano, Valentina Gliozzi, Andrea La Spisa, Nicola Olivetti, Gian Luca Pozzato This file is part of KLMOptimal. KLMOptimal 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. KLMOptimal 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 KLMOptimal. If not, see . */ /* Theorem prover for KLM Preferential logic P */ :- op(400,fy,neg), op(400,fy,box), op(500,xfy,and), op(600,xfy,or), op(650,xfy,->), op(650,xfy,<->), op(650,xfy,=>). :-use_module(library(lists)). /* --------------------------------------------------------------------------------------- */ /* Top level procedure klmoptimal klmoptimal(KB,Tree):- KB is unsatisfiable in Preferential logic P Tree is a closed tableau for KB */ klmoptimal(KB,Tree):- extract_neg_cond(KB,KB1,L),!, member(neg(A=>B),L), prove([neg B|[box neg A|[A|KB1]]],[],Tree). /* extract_neg_cond(KB,KB1,L):-builds the list L of negated conditionals neg (A=>B) belonging to KB. As a side effect, the list KB1 is KB \ L */ extract_neg_cond([],[],[]):-!. extract_neg_cond([neg (A => B)|Tail],KB1Tail,[neg (A=> B)|LTail]):-!, extract_neg_cond(Tail,KB1Tail,LTail). extract_neg_cond([F|Tail],[F|KB1Tail],LTail):- extract_neg_cond(Tail,KB1Tail,LTail). /* prove(Gamma,Sigma,Tree) implements the tableau calculus T^P_T with the ([]-s) rule for building multilinear models */ prove(Gamma,_,tree(axiom)):-member(neg F,Gamma),member(F, Gamma),!. prove(Gamma,Sigma,tree(andP,F and G,SubTree)):-select(F and G,Gamma,NewGamma),!, prove([F|[G|NewGamma]],Sigma,SubTree). prove(Gamma,Sigma,tree(orN,neg(F or G),SubTree)):-select(neg (F or G),Gamma,NewGamma),!, prove([neg F|[neg G|NewGamma]],Sigma,SubTree). prove(Gamma,Sigma,tree(impN,neg (F -> G),SubTree)):-select(neg (F -> G),Gamma,NewGamma),!, prove([F|[neg G|NewGamma]],Sigma,SubTree). prove(Gamma,Sigma,tree(neg,neg neg F,SubTree)):-select(neg neg F,Gamma,NewGamma),!, prove([F|NewGamma],Sigma,SubTree). prove(Gamma,Sigma,tree(bimpP,F <-> G,SubTree)):-select(F <-> G,Gamma,NewGamma),!, prove([G->F|[F->G|NewGamma]],Sigma,SubTree). prove(Gamma,Sigma,tree(andN,neg (F and G),Sub1,Sub2)):-select(neg (F and G),Gamma,NewGamma),!, prove([neg F|NewGamma],Sigma,Sub1),!, prove([neg G|NewGamma],Sigma,Sub2). prove(Gamma,Sigma,tree(orP,F or G,Sub1,Sub2)):-select(F or G,Gamma,NewGamma),!, prove([F|NewGamma],Sigma,Sub1),!, prove([G|NewGamma],Sigma,Sub2). prove(Gamma,Sigma,tree(impN,F -> G,Sub1,Sub2)):-select(F -> G,Gamma,NewGamma),!, prove([neg F|NewGamma],Sigma,Sub1),!, prove([G|NewGamma],Sigma,Sub2). prove(Gamma,Sigma,tree(bimpN,neg (F <-> G),Sub1,Sub2)):-select(neg (F <-> G),Gamma,NewGamma),!, prove([neg (F->G)|NewGamma],Sigma,Sub1),!, prove([neg (G->F)|NewGamma],Sigma,Sub2). prove(Gamma,Sigma,tree(entP,A=>B,Sub1,Sub2,Sub3)):-select(A => B,Gamma,NewGamma),!, prove([neg A|NewGamma],[A => B|Sigma],Sub1),!, prove([neg box neg A|NewGamma],[A => B|Sigma],Sub2),!, prove([B|NewGamma],[A => B|Sigma],Sub3). /* Clause implementing the strenghtened version of ([]^-): an auxiliary predicate prove_neg_box is invoked in order to recursively apply the prove predicate on each conclusion of the rule */ prove(Gamma,Sigma,tree(boxN,ListOfTrees)):-member(neg box neg _,Gamma),!, extract_neg_boxes(Gamma,LBoxes), conditionals(Gamma,CondGamma), boxes(Gamma,Boxed,InBoxed), append(CondGamma,Sigma,Temp), append(Temp,Boxed,Temp2), append(Temp2,InBoxed,Node), prove_neg_box(LBoxes,Node,LBoxes,ListOfTrees). /* Auxiliary predicates */ /* prove_neg_box(LNBox,Node,ListaInteraNBox,ListOfTrees):- given the list LNBox of neg box neg A_i belonging to the current node of the tableau, this predicate invokes the prove predicate for each neg box neg A_i. For a specific neg box neg A_i, the conclusion contains: A, box neg A + B or neg box neg B for all the other neg box neg B in the initial list (ListaInteraBox), computed by the predicate solve_boxes */ prove_neg_box([],_,_,[]):-!. prove_neg_box([neg box neg A|Tail],Node,ListaInteraNBox,[SubTree|ListOfTrees]):- select(neg box neg A,ListaInteraNBox,NegOK),!, solve_boxes(NegOK,Temp), append(Node,Temp,Temp2), prove([A|[box neg A|Temp2]],[],SubTree), prove_neg_box(Tail,Node,ListaInteraNBox,ListOfTrees). solve_boxes([],[]):-!. solve_boxes([neg box neg B|Tail],[B or neg box neg B|ResTail]):-!,solve_boxes(Tail,ResTail). /* extract_neg_boxes(L,L1):-extracts from L formulas neg box neg A, building the list L1 */ extract_neg_boxes([],[]):-!. extract_neg_boxes([neg box neg A|Tail],[neg box neg A|BoxTail]):-!,extract_neg_boxes(Tail,BoxTail). extract_neg_boxes([_|Tail],BoxTail):-extract_neg_boxes(Tail,BoxTail). /* conditionals(L,L1):-extracts from L formulas A=>B, building the list L1 */ conditionals([],[]):-!. conditionals([A => B|Tail],[A => B|CondTail]):-!,conditionals(Tail,CondTail). conditionals([_|Tail],CondTail):-conditionals(Tail,CondTail). /* boxes(L,LBox,LArg):-extracts from L formulas box neg A, building the list LBox. The list LArg also contains formulas in the scope of box, i.e. neg A. */ boxes([],[],[]):-!. boxes([box neg A|Tail],[box neg A|BoxTail],[neg A|ArgTail]):-!,boxes(Tail,BoxTail,ArgTail). boxes([_|Tail],BoxTail,ArgTail):-boxes(Tail,BoxTail,ArgTail).