/* See file "instruction" on how to use this program */ /* computes closed-formed solution from a set of effect axioms and causal rules. Uses on snc/5 and wsc/5 for computing the strongest necessary and weakest sufficient conditions of a proposition. future work: 1. try to delay propositionization as late as possible; 2. try to generate a first-order s.s.a. from propositional ones; 3. detect impossible actions by checking the consistency of init_axiom(A), and the regression of causal constraints in the successor situation; (some limited consistency check is already done) 4. right now we only use unit resolution in computing wsc (used in cnf_simplifies). in some applications, one may have to to use a more powerful procedure (e.g. use PD procedure to check if a given set of clauses is satisfiable or not). */ /* put in axioms about initial situation speeds up the computation of snc and wsc but returns more complicated formula that should be simplified using the init_axioms */ /* February 1999 */ /* defined fluents cannot occur in the heads of causal rules and effect axioms. They can occur in the bodies, and in action preconditions */ :- style_check(-singleton). :- style_check(-discontiguous). /* logical operators: - (not), & (and), \/ (or), -> (implies), <-> (iff) */ :- op(500,fx,-). :- op(780,xfy,&). :- op(790,xfy,\/). :- op(800,xfy,->). :- op(800,xfy,<->). /* quantifiers: all(var, dom, wff) (for all var in dom, wff is true) and some(var, dom, wff) */ /* variables need to be constants in prolog, and a variable cannot be used for more than once: all(x, block(x), all(x, block(x), on(x,Y)) is not allowed. The right way of encoding that one is all(x1, block(x1), all(x, block(x), on(x,Y)). */ /* quantifiers */ :- dynamic(all/3). :- dynamic(some/3). /* defined fluent definition */ :- dynamic(defined/2). /* This program uses nine databases: init_clause0(X), the set of clauses about the initial situation generated from causal rules and constraints; pseudo_ssa0(X), pseudo successor state axioms from causal rules; init_unit(X), the set of unit clauses derived from init_clause0 and action preconditions; init_clause(X), the set of non-unit clauses derived from init_clause0 and action preconditions; ssa(X), the dynamically computed successor state axioms; pseudo_ssa(X), the dynamically generated pseudo successor state axioms that are yet to be solved poss0(A,W) - action precondition after quantifiers are eliminated. effect0(A,C,E) - like poss0. causes0(C,E) - like poss0. */ :- dynamic(poss0/2). :- dynamic(effect0/3). :- dynamic(causes0/2). :- dynamic(init_clause0/1). :- dynamic(init_unit/1). :- dynamic(init_clause/1). :- dynamic(ssa/1). :- dynamic(pseudo_ssa/1). :- dynamic(non_frame_ssa/1). /* solve the equations one by one: 1. eliminate all those that already are in the right form. 2. if succ(F) <=> init(F) & W, then try to see if init(F) => succ(F) by substituting all the succ(f) propositions in W according to their pseudo s.s.a., and try to reduce the new W to true by adding init(F) to InitDB. if so, then we have succ(F) <=> init(F), a frame axiom. 3. for the remaining ones, use the expensive snc and wsc procedure. */ solve :- write_ln('input: '), read(user_input,Input), consult(Input), string_concat(Input, '-out.sht',Out11), string_to_atom(Out11,Out1), write('output in Strips format in file '), write(Out1), nl, string_concat(Input, '-out.lng',Out22), string_to_atom(Out22,Out2), write('output complete axioms in file '), write(Out2), nl, open(Out1,write,out1), open(Out2,write,out2), poss, effect, causes, init_axiom0, generating_ssa0, findall(_, (action(A), nl(out1), write(out1,'Action '), write(out1,A), nl(out1), nl(out1), nl(out2), write(out2,'Action '), write(out2,A), nl(out2), nl(out2), init_axiom(A), ((init_clause([[]]), write(out1,'Impossible action'), nl(out1), nl(out1), write(out2,'Impossible action'), nl(out2), nl(out2), action_cleanup, fail); (init_clause(XY), XY\==[[]])), generating_ssa(A), processing_ssa1, assert(inf(I3)), frame_axiom, processing_ssa2(A), /*bottle neck for context-dependent actions */ processing_ssa3, /* for defined fluents */ forall(ssa(X),(write(out2,X),nl(out2))), poss_list(out1,A), add_list(out1), delete_list(out1), conditional_list(out1), indeterminate_list(out1), action_cleanup ), _), cleanup, close(out1), close(out2). action_cleanup :- retractall(inf(_)), retractall(ssa(_)), retractall(pseudo_ssa(_)), retractall(init_unit(_)), retractall(init_clause(_)). /* get rid of quantifications */ elim_quant(-W1,-W2) :- elim_quant(W1,W2), !. elim_quant(W1->W2, W11->W22) :- elim_quant(W1,W11), elim_quant(W2,W22), !. elim_quant(W1 | W2, W11 | W22) :- elim_quant(W1,W11), elim_quant(W2,W22), !. elim_quant(W1\/W2, W11\/W22) :- elim_quant(W1,W11), elim_quant(W2,W22), !. elim_quant(W1&W2, W11&W22) :- elim_quant(W1,W11), elim_quant(W2,W22), !. elim_quant(W1<->W2, W11<->W22) :- elim_quant(W1,W11), elim_quant(W2,W22), !. elim_quant(all(V,D,W), NewW) :- subst_var(D1,V,D,X), free_variables(D1,[X1]), findall(X1,D1,Domain), findall(Y, (member(Z,Domain), subst_var(Y,V,W,Z)), ConjL), list2conjunct(ConjL,W1), elim_quant(W1,NewW), !. elim_quant(some(V,D,W), NewW) :- subst_var(D1,V,D,X), free_variables(D1,[X1]), findall(X1,D1,Domain), findall(Y, (member(Z,Domain), subst_var(Y,V,W,Z)), DisjL), list2disjunct(DisjL,W1), elim_quant(W1,NewW), !. elim_quant(W,W) :- !. /* eliminate defined fluents */ elim_defined(F,C) :- defined(F,C), !. elim_defined(-W1,-W2) :- elim_defined(W1,W2), !. elim_defined(W1->W2, W11->W22) :- elim_defined(W1,W11), elim_defined(W2,W22), !. elim_defined(W1 | W2, W11 | W22) :- elim_defined(W1,W11), elim_defined(W2,W22), !. elim_defined(W1\/W2, W11\/W22) :- elim_defined(W1,W11), elim_defined(W2,W22), !. elim_defined(W1&W2, W11&W22) :- elim_defined(W1,W11), elim_defined(W2,W22), !. elim_defined(W1<->W2, W11<->W22) :- elim_defined(W1,W11), elim_defined(W2,W22), !. elim_defined(all(V,D,W), all(V,D,NewW)) :- elim_defined(W,NewW), !. elim_defined(some(V,D,W), some(V,D,NewW)) :- elim_defined(W,NewW), !. elim_defined(W,W) :- !. /* building poss0, effect0, and causes0 */ poss :- findall(_, (action(A),poss(A,W), elim_quant(W,W1), assert(poss0(A,W1))), _). effect :- findall(_, (action(A),effect(A,C,E), elim_quant(C,C1), assert(effect0(A,C1,E))),_). causes :- findall(_, (causes(C,E), elim_defined(C,C2), elim_quant(C2,C1), assert(causes0(C1,E))),_). /* the set of propositions is given by prop/1 */ :- dynamic(prop/1). prop(true). prop(false). /* fluent(p) if p is a ground propositional fluent */ /* static(p) if p is a proposition that is not affacted by any actions */ :- dynamic(fluent/1). :- dynamic(static/1). /* static propositions are propositions */ prop(X) :- static(X). /* generates propositions about the initial and successor situations */ prop(init(F)) :- fluent(F). prop(succ(F)) :- fluent(F). /* constraints - those that do not yield indirect effects but but yield implicit action preconditions (not computed for now), and those constraints on static fluents are given by axioms */ :- dynamic(axiom/1). /* effect axioms and causal rules */ :- dynamic(effect/3). /* effect(Action,Wff,Literal): use effect(Action,true,F) and effect(Action, true, -F)*/ :- dynamic(causes/2). /* causes(Wff,Literal) */ /* generating the initial set of pseudo s.s.a. for primitive fluents using only causal rules */ generating_ssa0 :- findall(_, (fluent(F), \+ defined(F,_), findall(X, (causes0(C,F), fluent2succ(C,X)), PosL), findall(X1, (causes0(C1,-F), fluent2succ(C1,X1)), NegL), list2disjunct(PosL,Pos), list2disjunct(NegL,Neg), assert(pseudo_ssa0(succ(F) <-> (Pos \/ (init(F) & -Neg))))),_). /* generating the initial axioms from causal rules and defined fluent definitions*/ init_axiom0 :- findall(A, (causes0(C,L), fluent2init(C,C1), ((L=(-F), A=(C1 -> -init(F))); A=(C1->init(L))), !), T1), findall(A1, (defined(F1,Def), elim_quant(Def,Def1), fluent2init(Def1,W), A1=(init(F1)<->W)), T2), append(T1,T2,T3), findall(W, (axiom(W0), fluent2init(W0,W)), T4), append(T3,T4,T), init_theory2cnf(T,CNF), cnf_sort_simpl(CNF,CNF1), sort(CNF1,CNF2), assert(init_clause0(CNF2)). /* for a given action A, this generates init_unit and init_clause by unit resolution */ /* InitDB1=[[]] when Unit+InitDB1 is (obviously) inconsistent */ init_axiom(A) :- findall(W, (poss0(A,X), fluent2init(X,W)), T), ((T=[], T1=[false]); (T\==[], T1=T)), init_theory2cnf(T1, CNF), init_clause0(CNF2), append(CNF,CNF2,CNF3), cnf_sort_simpl(CNF3,CNF10), sort(CNF10,CNF11), divide_unit(CNF11,Unit0,CNF1), unit_conseq(CNF1,Unit0, Unit, InitDB), cnf_sort_simpl(InitDB,InitDB1), assert(init_unit(Unit)), assert(init_clause(InitDB1)). /* divide a set of clauses into unit and non-unit subsets */ divide_unit([],[],[]) :- !. divide_unit([C|CNF], [P|Unit], NewCNF) :- C=[P], !, divide_unit(CNF, Unit, NewCNF). divide_unit([C|CNF], Unit, [C|NewCNF]) :- divide_unit(CNF, Unit, NewCNF). /* given an action, this generates an initial set of s.s.a. and pseudo s.s.a. for primitive fluents (assume that generating_ssa0 and init_axiom(A) has already been run) */ generating_ssa(A) :- init_unit(Unit), findall(_, (pseudo_ssa0(succ(F)<->(W1 \/ (init(F)&W2))), findall(X, (effect0(A,C,F), fluent2init(C,X)), PosL), findall(X1, (effect0(A,C1,-F), fluent2init(C1,X1)), NegL), list2disjunct(PosL, Pos), list2disjunct(NegL, Neg), init_simplifying0(Pos,Pos1,Unit), init_simplifying0(Neg,Neg1,Unit), (((member(init(F),Unit), simplifies(Pos1\/W1\/(W2& -Neg1),W)); (member(-init(F),Unit), simplifies(Pos1\/W1,W)); simplifies(Pos1\/W1\/(init(F) & W2 & -Neg1),W) ), !), ((occurrs(succ(F1),W), assert(pseudo_ssa(succ(F)<->W))); assert(ssa(succ(F)<->W))),!), _). /* solve(A) for solving one action */ solve(A) :- poss, effect, causes, init_axiom0, generating_ssa0, init_axiom(A), generating_ssa(A), processing_ssa1, I3=0, assert(inf(I3)), frame_axiom, processing_ssa2(A), /*bottle neck for context-dependent actions */ processing_ssa3, action_cleanup, cleanup. /* print out run time statictics */ report(Stream,X,I1,I0) :- I2 is I1-I0, format(Stream,'~w~t~D~30|~n',[X,I2]). /* write poss conditions */ poss_list(Out,Action) :- write(Out, 'Preconditions:'), nl(Out), nl(Out), forall(poss0(Action,X), (write(Out,X), nl(Out))), nl(Out). /* write add list (use init_unit to filter away those that are already true in the initial situation */ add_list(Out) :- write(Out, 'Add list:'), nl(Out), nl(Out), init_unit(Unit), findall(_, (ssa(Y), Y=(succ(X)<->true), \+ member(init(X),Unit), write(Out,X),nl(Out)),_), nl(Out). /* write delete list (use init_unit to filter away those that are already false in the initial situation */ delete_list(Out) :- write(Out, 'Delete list:'), nl(Out), nl(Out), init_unit(Unit), findall(_, (ssa(Y), Y=(succ(X)<->false), \+ member(-init(X), Unit), write(Out,X),nl(Out)),_), nl(Out). conditional_list(Out) :- write(Out, 'Conditional effects:'), nl(Out), nl(Out), findall(_, (ssa(Y), Y=(succ(X)<->W), W\==true,W\==false,W\==init(X), write(Out,Y),nl(Out)),_), nl(Out). indeterminate_list(Out) :- write(Out, 'Indeterminate effects:'), nl(Out), nl(Out), findall(_, (ssa(Y), (Y=(succ(X)->W); Y=(W->succ(X))), write(Out,Y),nl(Out)),_), nl(Out). /* for each s.s.a in pseudo_ssa(), if it mentions succ(F), and there is a s.s.a. for F in ssa(), then get rid of this succ(F). */ processing_ssa1 :- findall(X,ssa(X),SSA), processing_ssa1(SSA). processing_ssa1(SSA) :- findall(X, (pseudo_ssa(succ(F)<->Left), set_subst(Left,SSA,Left1), simplifies(Left1,Left2), X=(succ(F)<->Left2)), Succ), split(Succ,SSA1,Succ1), ((SSA1=[], retractall(pseudo_ssa(_)), forall(member(S,Succ1),assert(pseudo_ssa(S)))); (retractall(pseudo_ssa(_)), forall(member(S1,Succ1), assert(pseudo_ssa(S1))), forall(member(S2,SSA1), assert(ssa(S2))), processing_ssa1(SSA1))), !. /* try frame axioms candidates (those having the form succ(F)<->init(F) & W) */ frame_axiom :- init_clause(InitDB), findall(_, (pseudo_ssa(succ(F)<->init(F)&WF), unit_conseq(InitDB,[init(F)],Unit,_), regress_init_simplifying(WF,WF1,Unit), retract(pseudo_ssa(succ(F)<->init(F)&WF)), (((WF1=true, assert(ssa(succ(F)<->init(F)))); (member(false,Unit), assert(ssa(succ(F)<->init(F)))); (assert(non_frame_ssa(succ(F)<->init(F)&WF)), fail)), !), /*if WF1\=true, then this pseudo-ssa is unlikely to be solved this way, so don't try it anymore by moving it into another database*/ findall(S1, (pseudo_ssa(S), subst(S1,succ(F),S,init(F))), TempSSA), retractall(pseudo_ssa(_)), forall(member(S2,TempSSA), assert(pseudo_ssa(S2))), findall(S3, (non_frame_ssa(S4), subst(S3,succ(F),S4,init(F))), TempSSA1), retractall(non_frame_ssa(_)), forall(member(S5,TempSSA1), assert(non_frame_ssa(S5))) ),_), forall(non_frame_ssa(S6), assert(pseudo_ssa(S6))), retractall(non_frame_ssa(_)). /* for the remaining axioms in pseudo_ssa(), use snc and wsc to solve the equations */ processing_ssa2(A) :- findall(succ(F1), pseudo_ssa(succ(F1)<->_), Succ), init_unit(Unit), findall([U],member(U,Unit),UnitCNF), init_clause(C), append(UnitCNF,C,Init), forall(pseudo_ssa(succ(F)<->Left), (findall(X, (pseudo_ssa(X), X\== (succ(F)<->Left)), Axiom), init_theory2cnf(Axiom,CNF), cnf_sort_simpl(CNF,CNF1), disjunct_set(Left,DL), findall(SNC, (member(Case, DL), init_theory2cnf([Case],CNF2), /* same as using succ(F)->Case and then let succ(F)=true */ cnf_sort_simpl(CNF2,CNF3), append(CNF3,CNF1,CNF4), snc(succ(F),SNC,Succ, CNF4,Init)), SncL), list2disjunct(SncL,W), init_theory2cnf([-(Left)],CNF5), /* same as using Left->succ(F) and then let succ(F)=false */ cnf_sort_simpl(CNF5,CNF6), append(CNF6,CNF1,CNF7), init_theory2cnf([W],CNF8), cnf_sort_simpl(CNF8,CNF9), append(CNF9,Init,Init1), wsc(succ(F),W1,Succ,CNF7,Init1), ((W1=true, assert(ssa(succ(F)<->W))); (assert(ssa(succ(F)->W)), assert(ssa((W&W1)->succ(F))))), ! )). /* compute ssa for defined fluents */ processing_ssa3 :- findall(X,ssa(X),Succ), init_unit(Unit), findall(_, (defined(F,W), elim_quant(W,W1), ((persistent(W1,Succ,Unit), assert(ssa(succ(F)<->init(F)))); (static_unit_simplifying(W1,W11,Unit), fluent2succ(W11,W2), set_subst(W2,Succ,W3), simplifies(W3,W4), assert(ssa(succ(F)<->W4)) )), !), _). /* persistent(W,Succ,Unit) if all the fluents in W persist according to Succ */ persistent(W,Succ,Unit) :- \+ (occurrs(F,W), fluent(F), \+ fluent_persistent(F,Succ,Unit)). fluent_persistent(F,Succ,Unit) :- member(succ(F)<->init(F), Succ). fluent_persistent(F,Succ,Unit) :- member(succ(F)<->true, Succ), member(init(F),Unit). fluent_persistent(F,Succ,Unit) :- member(succ(F)<->false, Succ), member(-init(F),Unit). /* find the set of disjuntions of a formula */ disjunct_set((Case\/W), [Case|DL]) :- disjunct_set(W,DL), !. disjunct_set(W,[W]). /* clean up databases */ cleanup :- retractall(non_frame_ssa(_)), retractall(pseudo_ssa(_)), retractall(pseudo_ssa0(_)), retractall(init_clause0(_)), retractall(init_unit(_)), retractall(init_clause(_)), retractall(ssa(_)), retractall(inf(_)), retractall(poss0(_,_)), retractall(effect0(_,_,_)), retractall(causes0(_,_)). /* partial regress (like set_subst) and then init_simplifying */ regress_init_simplifying(W,NewW,Unit) :- findall(X, (occurrs(succ(F),W), ((pseudo_ssa(succ(F)<->WF);non_frame_ssa(succ(F)<->WF)),!), init_simplifying0(WF,WF1,Unit), X=(succ(F)<->WF1)), Succ1), init_simplifying0(W,W1,Unit), set_subst(W1,Succ1,W2), simplifies(W2,NewW). /* replace succ(f) in a formula according to successor state axioms in Suc (partial regression) */ set_subst(Left,[],Left). set_subst(Left, [succ(F)<->W|Succ], NewLeft) :- subst(Left1,succ(F),Left,W), set_subst(Left1,Succ,NewLeft). /* split a set of pseudo successor state axioms into two sets, one contains real successor state axioms, the other the remaining ones. */ split([],[],[]). split([X<->Left | Succ],Done, [X<->Left|NewSucc]) :- fluent(F), occurrs(succ(F),Left), !, split(Succ,Done,NewSucc). split([X<->Left | Succ],[X<->Left|Done],NewSucc) :- split(Succ,Done,NewSucc). /* simplifying a formula by getting rid of true, false, and literals that are already true in the initial situation */ init_simplifying(W,NewW,[]) :- simplifies(W,NewW). init_simplifying(W,NewW, [P|Unit]) :- prop(P), subst(W1,P,W,true), init_simplifying(W1,NewW,Unit), !. init_simplifying(W,NewW, [- P|Unit]) :- prop(P), subst(W1,P,W,false), init_simplifying(W1,NewW,Unit), !. init_simplifying(W,NewW, [_|Unit]) :- init_simplifying(W,NewW,Unit), !. /* this version of simplifying is useful when not many unit clauses in IUnit occurrs in W (it's used in pre_succ_axiom) */ init_simplifying0(W,NewW,IUnit) :- findall(X, (occurrs(P,W), ((member(-P,IUnit), X=(-P)); (member(P,IUnit), X=P)),!), NewUnit), /* write(NewUnit),nl, */ sort(NewUnit, NewUnit1), init_simplifying(W,NewW,NewUnit1). /* simplifying a formula by getting rid of true, false, and unit clauses */ static_unit_simplifying(W,W,[]) :- !. static_unit_simplifying(W,NewW, [X|Unit]) :- static(X), !, subst(W1,X,W,true), static_unit_simplifying(W1,NewW,Unit), !. static_unit_simplifying(W,NewW, [- X|Unit]) :- static(X), !, subst(W1,X,W,false), static_unit_simplifying(W1,NewW,Unit). static_unit_simplifying(W,NewW, [_|Unit]) :- static_unit_simplifying(W,NewW,Unit), !. /* subst(NewW,P,W,Q): NewW is the result of replacing P in W by Q */ subst(W,P,P,W) :- !. subst(Q,P,Q,W) :- (prop(Q);fluent(Q)), !. subst(-NewW, P, -W, Q) :- subst(NewW, P, W, Q), !. subst(NewW1 \/ NewW2, P, W1 \/ W2, Q) :- subst(NewW1, P, W1, Q), subst(NewW2, P, W2, Q), !. subst(NewW1 & NewW2, P, W1 & W2, Q) :- subst(NewW1, P, W1, Q), subst(NewW2, P, W2, Q), !. subst(NewW1 -> NewW2, P, W1 -> W2, Q) :- subst(NewW1, P, W1, Q), subst(NewW2, P, W2, Q), !. subst(NewW1 <-> NewW2, P, W1 <-> W2, Q) :- subst(NewW1, P, W1, Q), subst(NewW2, P, W2, Q), !. /* subst_var(NewW,P,W,Q): NewW is the result of replacing the variable P in W by Q */ subst_var(W,P,P,W) :- !. subst_var(NewW, P, W, Q) :- W =.. [Functor | Args], findall(NewArg, (member(Arg, Args), subst_var(NewArg,P,Arg,Q)), NewArgs), NewW =.. [Functor | NewArgs]. /* fluent2init and fluent2succ */ fluent2init(true, true) :- !. fluent2init(false, false) :- !. fluent2init(P,P) :- static(P), !. fluent2init(F, init(F)) :- fluent(F), !. fluent2init(-F, -W) :- fluent2init(F,W), !. fluent2init(F1 \/ F2, W1 \/ W2) :- fluent2init(F1,W1), fluent2init(F2,W2), !. fluent2init(F1 & F2, W1 & W2) :- fluent2init(F1,W1), fluent2init(F2,W2), !. fluent2init(F1 -> F2, W1 -> W2) :- fluent2init(F1,W1), fluent2init(F2,W2), !. fluent2init(F1 <-> F2, W1 <-> W2) :- fluent2init(F1,W1), fluent2init(F2,W2), !. fluent2init(F,true) :- F =.. [= | _], F, !. fluent2init(F,true) :- F =.. [== | _], F, !. fluent2init(F,true) :- F =.. [\== | _], F, !. fluent2init(F,false) :- F =.. [= | _]. fluent2init(F,false) :- F =.. [== | _]. fluent2init(F,false) :- F =.. [\== | _]. fluent2succ(true, true) :- !. fluent2succ(false, false) :- !. fluent2succ(P,P) :- static(P), !. fluent2succ(F, succ(F)) :- fluent(F), !. fluent2succ(-F, -W) :- fluent2succ(F,W), !. fluent2succ(F1 \/ F2, W1 \/ W2) :- fluent2succ(F1,W1), fluent2succ(F2,W2), !. fluent2succ(F1 & F2, W1 & W2) :- fluent2succ(F1,W1), fluent2succ(F2,W2), !. fluent2succ(F1 -> F2, W1 -> W2) :- fluent2succ(F1,W1), fluent2succ(F2,W2), !. fluent2succ(F1 <-> F2, W1 <-> W2) :- fluent2succ(F1,W1), fluent2succ(F2,W2), !. fluent2succ(F,true) :- F =.. [= | _], F, !. fluent2succ(F,true) :- F =.. [== | _], F, !. fluent2succ(F,true) :- F =.. [\== | _], F, !. fluent2succ(F,false) :- F =.. [= | _]. fluent2succ(F,false) :- F =.. [== | _]. fluent2succ(F,false) :- F =.. [\== | _]. /* snc of a proposition: snc(Q,W,B,CNF,BaseCNF) if W is the SNC of Q on propositions that are not in B in theory CNF + BaseCNF (both given as CNFs) with the requirement that BaseCNF must not mention any propositions in B so that W computed is simplified using it */ snc(Q,W,B,CNF,BaseCNF) :- resolve(CNF,Q,CNF1), /* append(BaseCNF,CNF1,CNF2): try not to use BaseCNF*/ forget(CNF1, B, CNF3), cnf_all_subsumes(CNF3,BaseCNF,CNF4), init_minimize(CNF4,BaseCNF,NewCNF), cnf2wff(NewCNF, W). /* init_minimize(CNF4,CNF6,NewCNF):eliminate clauses in CNF4 that are redundant in the sense that it is subsumed by the rest of the clauses in CNF4 and CNF6 */ init_minimize(CNF1,CNF2,NewCNF) :- member(C,CNF1), difference(CNF1,C,CNF3), union(CNF3,CNF2,CNF4), cnf_simplifies(CNF4,CNF5), member(C1,CNF5), cnf_subsumes(C1,C), !, init_minimize(CNF3,CNF2,NewCNF). init_minimize(CNF,_,CNF). /* cnf_all_subsumes(CNF3,CNF2,NewCNF): eliminate clauses in CNF3 that are subsumed by those in CNF2 */ cnf_all_subsumes([],_,[]). cnf_all_subsumes([C|CNF], CNF1, CNF2) :- member(C1,CNF1), cnf_subsumes(C1,C), !, cnf_all_subsumes(CNF,CNF1,CNF2). cnf_all_subsumes([C|CNF], CNF1, [C | CNF2]) :- cnf_all_subsumes(CNF,CNF1,CNF2). /* wsc of a proposition */ /* wsc of a proposition: wsc(Q,W,B,CNF,BaseCNF) if W is the WSC of Q on propositions that are not in B in theory CNF + BaseCNF (both given as CNFs) with the requirement that BaseCNF must not mention any propositions in B so that W computed is simplified using it */ wsc(Q,W,B,CNF,BaseCNF) :- resolve(CNF,-Q,CNF1), append(BaseCNF,CNF1,CNF2), cnf_simplifies(CNF2, CNF22), forget(CNF22, B, CNF3), cnf_simplifies(CNF3,CNF33), cnf_all_subsumes(CNF33,BaseCNF,CNF4), negate(CNF4, DNF), !, dnf2wff(DNF, W). /* init_theory2cnf(T,CNF) transforms a theory T to a CNF */ init_theory2cnf([],[]). init_theory2cnf([A|T],CNF) :- wff2cnf(A,CNF1), init_theory2cnf(T,CNF2), union(CNF1,CNF2,CNF). /* resolve a literal in a CNF */ resolve([],_,[]). resolve([C|CNF], P, NewCNF) :- member(P,C), !, resolve(CNF,P,NewCNF). resolve([C|CNF], P, [NewC|NewCNF]) :- complement(P,P1), difference(C,P1,NewC), resolve(CNF,P,NewCNF). /* forget(A,B,C): C is the result forgetting all the propositions in B from formula A. We assume that A is in CNF. C is also given out in CNF. The key is in the heuristic of deciding which proposition in B to forget first */ forget(A, [], A) :- !. forget(A, PL, NewA) :- select(A, PL, P), difference(PL, P, NewPL), forget_one(A, P, NewA1), !, forget(NewA1, NewPL, NewA). /* forget_one(CNF1, P, CNF2): CNF2 is the result of forgetting P in CNF1 */ forget_one(CNF, P, NewCNF) :- split(CNF, P, CNF1, CNF2, CNF3), resolve(CNF2, P, CNF21), resolve(CNF1, -P, CNF11), cnf_simplifies(CNF21,CNF22), cnf_simplifies(CNF11,CNF12), cnf_disjunct(CNF12,CNF22,L), ((L=[], NewCNF=CNF3); (union(L, CNF3, CNF4), cnf_simplifies(CNF4, NewCNF))), !. /* split(CNF, P, CNF1, CNF2, CNF3): if CNF3 is the set of cluases in CNF that do not mention P and -P, CNF1 is those mention P, CNF2 is those mention -P */ split([], _, [], [], []). split([Clause|CNF], P, [Clause | CNF1], CNF2, CNF3) :- member(P, Clause), !, split(CNF, P, CNF1, CNF2, CNF3). split([Clause|CNF], P, CNF1, [Clause | CNF2], CNF3) :- member(-P, Clause), !, split(CNF, P, CNF1, CNF2, CNF3). split([Clause|CNF], P, CNF1, CNF2, [Clause | CNF3]) :- split(CNF, P, CNF1, CNF2, CNF3). /* cnf_disjunct(CNF1,CNF2,CNF3): if CNF3 is the CNF of CNF1 v CNF2 */ cnf_disjunct([],CNF2,[]) :- !. cnf_disjunct(CNF1,[],[]) :- !. cnf_disjunct([[]],CNF2,CNF2) :- !. cnf_disjunct(CNF1,[[]],CNF1) :- !. cnf_disjunct(CNF1,CNF2,CNF3) :- setof(X, Y^Z^(member(Y,CNF1), member(Z,CNF2), union(Y,Z,X)), CNF3). /* select first those that are already entailed */ select(CNF, PL, P) :- member(P,PL), member([P],CNF), !. select(CNF, PL, P) :- member(P,PL), member([-P],CNF), !. /* select in sequence given afterward */ select(_, [P|_], P) :- !. /* select(A, PL, P): if there is no other Q in PL such that forget(A; Q) is a shorter formula than forget(A; P). */ /* select(_, [P], P) :- !. select(A, PL, P) :- setof(X, Q^NewA^N^(member(Q, PL), basic_forget(A, Q, NewA), size(NewA, N), X=[N,Q]), [[_,P]|_]). */ /* size(A,N): N is the size of the formula A */ size(P,1) :- prop(P). size(-A, N) :- size(A, M), N is M+1. size(A\/B, N) :- size(A, N1), size(B, N2), N is N1+N2+1. size(A&B, N) :- size(A, N1), size(B, N2), N is N1+N2+1. size(A->B, N) :- size(A, N1), size(B, N2), N is N1+N2+1. size(A<->B, N) :- size(A, N1), size(B, N2), N is N1+N2+1. /* conjunct(T,CNF): takes the conjunction of all elements in T */ conjunct([], []). conjunct([CNF1|T], CNF2) :- conjunct(T, CNF3), union(CNF1, CNF3, CNF2). /* difference(L,P,L1): L1 is L - [P] */ difference([P | L], P, L) :- !. difference([Q | L], P, [Q | NewL]) :- difference(L,P,NewL). difference([],P,[]). /* wff2cnf transforms a wff to its conjunctive normal form in list format */ wff2cnf(P, [[P]]) :- prop(P), !. wff2cnf(-P, [[-P]]) :- prop(P), !. wff2cnf(P->Q, L) :- wff2cnf(-P\/Q, L), !. wff2cnf(P<->Q, L) :- wff2cnf((-P\/Q)&(-Q\/P), L), !. wff2cnf(P&Q, L) :- wff2cnf(P,L1), wff2cnf(Q,L2), append(L1,L2,L), !. wff2cnf(P\/Q, L) :- wff2cnf(P,L1), wff2cnf(Q,L2), findall(X, (member(Y,L1), member(Z,L2), append(Y,Z,X)), L), !. wff2cnf(-P, L) :- wff2dnf(P, L1), negate(L1, L), !. /* wff2cnf(W,NewW) :- negation_inside(W,W1), wff2cnf0(W1,NewW). */ wff2cnf0(P, [[P]]) :- prop(P), !. wff2cnf0(-P, [[-P]]) :- prop(P), !. wff2cnf0(P&Q, L) :- wff2cnf0(P,L1), wff2cnf0(Q,L2), union(L1,L2,L), !. wff2cnf0(P\/Q, L) :- wff2cnf0(P,L1), wff2cnf0(Q,L2), setof(X, Y^Z^(member(Y,L1), member(Z,L2), union(Y,Z,X)), L), !. /* move negation inside */ negation_inside(P,P) :- prop(P), !. negation_inside(-P,-P) :- prop(P), !. negation_inside(-(W1 & W2), W) :- negation_inside(-W1 \/ -W2, W), !. negation_inside(-(W1 \/ W2), W) :- negation_inside(-W1 & -W2, W), !. negation_inside(W1 -> W2, W) :- negation_inside(-W1 \/ W2, W), !. negation_inside(W1 <-> W2, W) :- negation_inside((-W1 \/ W2) & (-W2 \/ W1), W), !. negation_inside(W1 \/ W2, NewW1 \/ NewW2) :- negation_inside(W1,NewW1), negation_inside(W2,NewW2), !. negation_inside(W1 & W2, NewW1 & NewW2) :- negation_inside(W1,NewW1), negation_inside(W2,NewW2), !. /* wff2dnf transforms a wff to its disjunctive normal form in list format */ wff2dnf(P,[[P]]) :- prop(P), !. wff2dnf(-P,[[-P]]) :- prop(P), !. wff2dnf(P->Q, L) :- wff2dnf(-P\/Q, L). wff2dnf(P<->Q, L) :- wff2dnf((P->Q)&(Q->P), L). wff2dnf(P\/Q, L) :- wff2dnf(P,L1), wff2dnf(Q,L2), append(L1,L2,L). wff2dnf(P&Q, L) :- wff2dnf(P,L1), wff2dnf(Q,L2), findall(X, (member(Y,L1), member(Z,L2), append(Y,Z,X)), L). wff2dnf(-P, L) :- wff2cnf(P,L1), negate(L1,L). /* negate(L1,L): negate L1 in DNF (CNF) and make it into a CNF (DNF). */ negate([],[]) :- !. negate([[]],[[]]) :- !. negate(L1,L) :- bagof(X, Y^(member(Y, L1), negate_one_clause(Y,X)), L). /* negate_one_clause(L1, L2): make all elements in L1 into its complement */ negate_one_clause(L1, L2) :- bagof(X, Y^(member(Y,L1), complement(Y,X)), L2). complement(true,false) :- !. complement(false,true) :- !. complement(P,-P) :- prop(P). complement(-P,P) :- prop(P). /* dnf2wff(L,W) convert a DNF list to a formula */ dnf2wff([],false) :- !. dnf2wff([[]],true) :- !. dnf2wff([L], W) :- list2conjunct(L,W), !. dnf2wff([L1|L2], W1 \/ W2) :- list2conjunct(L1, W1), dnf2wff(L2,W2). /* cnf2wff(L,W) convert a CNF list to a formula */ cnf2wff([[]],false) :- !. cnf2wff([],true) :- !. cnf2wff([L], W) :- list2disjunct(L,W), !. cnf2wff([L1|L2], W1 & W2) :- list2disjunct(L1, W1), cnf2wff(L2,W2). /* list2conjunct(L,A): A is the conjunction of all formulas in L */ list2conjunct([P],P) :- !. list2conjunct([P | L],P & W) :- list2conjunct(L,W). /* list2disjunct(L,A): A is the disjunction of all formulas in L: A=false when L is empty */ list2disjunct(L, true) :- member(true,L), !. list2disjunct(L, true) :- member(-P,L), member(P,L), !. list2disjunct(L, W) :- sort(L,L1), delete(L1,false,L2), list2disj(L2,W), !. list2disj([], false) :- !. list2disj([P],P) :- !. list2disj([P | L],P \/ W) :- list2disj(L,W). /* cnf_simplifies(L,NewL): simplifies DNF L into L1 by eliminating repetitive literals and contradictive literals. It also eliminates clauses that subsumes others. */ cnf_simplifies(CNF, NewCNF) :- cnf_sort_simpl(CNF, CNF1), unit_elim(CNF1,CNF2), cnf_sort_simpl(CNF2, CNF3), check_contr(CNF3,CNF4), cnf_minimize(CNF4, NewCNF). /* sort each clause and get rid of tautologies */ cnf_sort_simpl([],[]). cnf_sort_simpl(CNF,[[]]) :- member([],CNF), !. cnf_sort_simpl(CNF,[[]]) :- member([false],CNF), !. cnf_sort_simpl(CNF,[[]]) :- member([-true],CNF), !. cnf_sort_simpl([C|CNF], NewCNF) :- member(true,C), !, cnf_sort_simpl(CNF, NewCNF). cnf_sort_simpl([C|CNF], NewCNF) :- member(-P,C), member(P,C), !, cnf_sort_simpl(CNF, NewCNF). cnf_sort_simpl([C|CNF], NewCNF) :- sort(C,NewC1), subtract(NewC1, [false,-true], NewC), ((NewC=[], NewCNF=[[]]); (cnf_sort_simpl(CNF, NewCNF1), NewCNF=[NewC|NewCNF1])), !. /* check for contradiction */ check_contr(CNF,[[]]) :- member([],CNF), !. check_contr(CNF,CNF). /* eliminates all unit clauses */ unit_elim(CNF,[[P]|NewCNF]) :- member([P],CNF), resolve(CNF,P,CNF2), !, unit_elim(CNF2,NewCNF), !. unit_elim(CNF,CNF) :- !. /* eliminates all unit clauses (keep the unit clauses deduced as a sep. arg. */ unit_elim(CNF,NewCNF,[P|Unit]) :- member([P],CNF), resolve(CNF,P,CNF2), !, unit_elim(CNF2,NewCNF,Unit), !. unit_elim(CNF,CNF,[]) :- !. /* generates the set of unit clause consequences from a set of non-unit clauses and a set of unit clauses using unit resolution (NewCNF is the remaining set of non-unit clauses, i.e. NewUnit + NewCNF is equivalent to CNF + Unit0) */ unit_conseq(CNF,[],[],CNF) :- !. unit_conseq(CNF,Unit0,[false],[[]]) :- member(false,Unit0), !. unit_conseq([[]],_,[false],[[]]) :- !. unit_conseq(CNF,Unit0,NewUnit,NewCNF) :- resolve_set(CNF,Unit0,CNF1,Unit1), unit_conseq(CNF1,Unit1,Unit2,NewCNF), append(Unit0,Unit1,Unit3), union(Unit3,Unit2,NewUnit), !. resolve_set([],Unit,[],[]) :- !. resolve_set([C|CNF],Unit,NewCNF,NewUnit) :- member(X,C), member(X,Unit), !, resolve_set(CNF,Unit,NewCNF,NewUnit), !. resolve_set([C|CNF],Unit,NewCNF,NewUnit) :- findall(X, (member(X,C), complement(X,X1), member(X1,Unit)), Set), subtract(C,Set,C1), ((C1=[P], resolve_set(CNF,Unit,NewCNF,Unit1), NewUnit=[P|Unit1]); (C1=[], %write('Inconsistent in resolve_set'), NewCNF=[[]], NewUnit=[false]); (resolve_set(CNF,Unit,CNF1,NewUnit), NewCNF=[C1|CNF1])), !. /* get rid of clauses that are subsumed by others. */ cnf_minimize(DNF,DNF1) :- member(L,DNF), member(L1,DNF), L\==L1, cnf_subsumes(L,L1), difference(DNF, L1, DNF2), cnf_minimize(DNF2,DNF1), !. cnf_minimize(DNF,DNF). /* cnf_subsumes(L,L1) if L subsumes L1: L is a subset of L1. */ cnf_subsumes(L,L1) :- \+ (member(X,L), X\==false, X\==(-true), \+ member(X,L1)). /* occurrs(P,W) if the proposition P occurrs in W */ occurrs(P,P) :- (prop(P);fluent(P)). occurrs(P, Q \/ R) :- occurrs(P,Q). occurrs(P, Q \/ R) :- occurrs(P,R). occurrs(P, Q & R) :- occurrs(P,Q). occurrs(P, Q & R) :- occurrs(P,R). occurrs(P, -Q) :- occurrs(P,Q). occurrs(P, Q -> R) :- occurrs(P,Q). occurrs(P, Q -> R) :- occurrs(P,R). occurrs(P, Q <-> R) :- occurrs(P,Q). occurrs(P, Q <-> R) :- occurrs(P,R). /* simplifies(W,NewW): simplifying W into NewW using logical rules about true and false */ simplifies(P, P) :- (prop(P);fluent(P)), !. simplifies(-W, NewW) :- simplifies(W, W1), ((W1=true, NewW=false); (W1=false, NewW=true); NewW=(-W1)), !. simplifies(W1 \/ W2, NewW) :- simplifies(W1, W11), simplifies(W2, W22), ((W11=true, NewW=true); (W22=true, NewW=true); (W11=false, NewW=W22); (W22=false, NewW=W11); (NewW= (W11 \/ W22))), !. simplifies(W1 & W2, NewW) :- simplifies(W1, NewW1), simplifies(W2, NewW2), ((NewW1=false, NewW=false); (NewW2=false, NewW=false); (NewW1=true, NewW=NewW2); (NewW2=true, NewW=NewW1); (NewW = (NewW1 & NewW2))), !. simplifies(W1 <-> W2, NewW) :- simplifies(W1, NewW1), simplifies(W2, NewW2), ((NewW1=true, NewW=NewW2); (NewW2=true, NewW=NewW1); (NewW1=false, NewW2=false, NewW = true); (NewW1=false, NewW = -NewW2); (NewW2=false, NewW = -NewW1); (NewW = (NewW1 <-> NewW2))), !. simplifies(P -> true, true) :- !. simplifies(true -> P, P1) :- simplifies(P,P1), !. simplifies(false -> P, true) :- !. simplifies(P -> false, P1) :- simplifies(-P,P1), !. simplifies(W1 -> W2, NewW) :- simplifies(W1, NewW1), simplifies(W2, NewW2), ((NewW1=false, NewW = true); (NewW2=true, NewW = true); (NewW1=true, NewW=NewW2); (NewW2=false, NewW = -NewW1); (NewW = (NewW1 -> NewW2))), !. /* old stuff */ /* compute all unit clauses that are true in the initial situation using forward chaining */ init_unit_clause :- retractall(init_unit_clause(_)), findall(X, init_unit_clause0(X), Unit0), init_unit_clause(Unit0, Unit), assert(init_unit_clause(Unit)). init_unit_clause(Unit1,Unit2) :- setof(X1, A^X^A1^(causes0(A,X), fluent2init(X,X1), \+ member(X1,Unit1), fluent2init(A,A1), init_simplifying(A1,true,Unit1)),Y), !, union(Unit1,Y,Unit11), init_unit_clause(Unit11,Unit2). init_unit_clause(Unit1,Unit1). init_unit_clause0(C) :- poss0(F), (fluent(F);(F=(-F1), fluent(F1))), fluent2init(F,C). init_unit_clause0(C) :- causes0(true,F), fluent2init(F,C). /* theory_simplifying(T,NewT) simplifies T into NewT by resolving all unit clauses and get rid of successor propositions succ(f) if there is already a sucessor state axiom for the fluent f */ /* get rid of unit clauses */ theory_simplifying(T,NewT) :- member(true,T), !, difference(T,true,T1), !, theory_simplifying(T1,NewT). theory_simplifying(T,[X|NewT]) :- member(X,T), prop(X), !, difference(T,X,T1), bagof(Y, Z1^Z2^(member(Z1,T1), subst(Z2,X,Z1,true), simplifies(Z2,Y)), T2), !, theory_simplifying(T2,NewT). theory_simplifying(T,[-X|NewT]) :- member(-X,T), prop(X), !, difference(T,-X,T1), bagof(Y, Z1^Z2^(member(Z1,T1), subst(Z2,X,Z1,false), simplifies(Z2,Y)), T2), !, theory_simplifying(T2,NewT). /* get rid of succ(f) for which there is already a successor state axiom */ theory_simplifying(T,[succ(F) <-> X | NewT]) :- member(succ(F) <-> X,T), fluent(F), \+ occurrs(succ(F1),X), !, difference(T, succ(F) <-> X, T1), bagof(Y, Z1^Z2^(member(Z1,T1), subst(Z2,succ(F),Z1,X), simplifies(Z2,Y)), T2), !, theory_simplifying(T2,NewT). theory_simplifying(T,T). /* pi - compute the prime implicates of a set of clauses */ pi(CNF,NewCNF) :- unit_elim(CNF,CNF1), /* apply unit resolution first */ member(C1,CNF1), member(C2,CNF1), C1\==C2, resolve_all(C1,C2,CNF2), not_subsumed(CNF2,CNF1,CNF3,CNF4), CNF3\==[], !, union(CNF3,CNF4,CNF5), pi(CNF5, NewCNF). pi(CNF,CNF). /* resolve two clauses */ resolve_all(C1,C2,CNF) :- findall(X, (member(P,C1), complement(P,Q), member(Q,C2), difference(C1,P,C11), difference(C2,Q,C21), union(C11,C21,C3), \+ (member(A,C3), member(-A,C3)), sort(C3,X)), CNF). not_subsumed(CNF2,CNF1,CNF3,CNF4) :- /* find first those clauses in CNF2 that is not subsumed by a clause in CNF1, and save them as CNF3, and then find those clauses in CNF1 that are not subsumed by a clause in CNF3, and store them in CNF4 */ findall(X, (member(X,CNF2), \+ (member(C,CNF1), subset(C,X))), CNF3), findall(X, (member(X,CNF1), \+ (member(C1,CNF3), subset(C1,X))), CNF4). /* find all relevant axioms: relevant_axiom(P,B,A) if A is the set of relevant axioms for computing the snc and wsc of P on B */ relevant_axiom(P,B,T) :- findall(X, axiom(X), T1), findall(Y, (axiom(Y), prop_of(Y,L1), (member(P,L1); subset(L1,[true,false|B]))), T2), subtract(T1,T2,T3), transitive_closure(T2,T3,B,T). /* compute the transitive closure of T1 in T2 */ transitive_closure(T1,T2,B,T3) :- member(A,T2), occurrs(P,A), \+ member(P,B), member(A1,T1), occurrs(P,A1), !, difference(T2,A,T4), transitive_closure([A|T1], T4,B,T3). transitive_closure(T,_,_,T). prop_of(A,L) :- findall(X, occurrs(X,A), L). /* :- initialization(solve). */