%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% Version: 1.00 Date: 15/03/98 File: defaults.pl %% Last Version: File: %% %% Changes: %% %% 18/03/95 Created %% %% 14/07/96 added configuration utilities %% 15/03/98 added pttp config and optional proof printing %% %% %% Purpose: %% %% %% %% Author: Torsten Schaub %% %% %% %% Usage: prolog defaults.pl %% %% %% %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- ensure_loaded(base). :- ensure_loaded(pttp). :- ensure_loaded(builtin). :- ensure_loaded(model). :- ensure_loaded(io). :- ensure_loaded(db). :- ensure_loaded(herbrand). :- ensure_loaded(hooks). :- ensure_loaded(lemma). :- ensure_loaded(xray_config). %%% ---------------------------------------------------------------------- %%% XRay COMPILATION (patches pttp) %%% Negation normal form/Defaults to Prolog clause translation. %%% Include a literal in the body of each clause to %%% indicate the number of the formula the clause came from. clauses((A , B),L,WffNum) :- !, clauses(A,L1,WffNum), WffNum2 is WffNum + 1, clauses(B,L2,WffNum2), conjoin(L1,L2,L). clauses( (Gamma :- Alpha : Beta) , L , WffNum ) :- !, clauses((Gamma :- gamma(WffNum,Gamma)),L1,WffNum), clauses((alpha(WffNum,Alpha) :- Alpha),L2,WffNum), conjoin(L1,L2,L3), conjoin(Gamma,Beta,C0), % ConDL-specific cnf(C0,C1), make_matrix(C1,C2), matrix_reduction(C2,Justification), (delta_ordering(compatibility>admissibility) -> conjoin(justification(Justification), alpha(WffNum,Alpha), Body); %true -> conjoin(alpha(WffNum,Alpha), justification(Justification), Body)), (compile_proof_printing -> Record = infer_by(default(WffNum:(Gamma :- Alpha : Justification))); %true -> Record = true), conjoin(Record,Body,Body1), DRule= (gamma(WffNum,Gamma) :- Body1), conjoin(DRule,L3,L). clauses(A,L,WffNum) :- head_literals(A,Lits), clauses(A,Lits,L,WffNum). clauses(A,[Lit|Lits],L,WffNum) :- body_for_head_literal(Lit,A,Body1), ((compile_proof_printing,Body1 = true) -> Record = infer_by(unit(WffNum:Lit)); compile_proof_printing -> Record = infer_by(extension(WffNum:Lit)); %true -> Record = true), conjoin(Record,Body1,Body), clauses(A,Lits,L1,WffNum), conjoin((Lit :- Body),L1,L). clauses(_,[],true,_). %%% This patches the original predicate %%% %%% add_ancestor((Head :- Body),(Head1 :- Body1)) :- functor(Head,query,_) -> Head1 = Head, add_ancestor_args(Body,[[],[],[]],Body1); functor(Head,gamma,_) -> Head =.. L, append(L,[_,_,Defaults],L1), Head1 =.. L1, add_ancestor_args(Body,[[],[],NewDefaults],Body2), conjoin((NewDefaults = [Head|Defaults]),Body2,Body1); functor(Head,alpha,_) -> Head =.. L, append(L,[_,_,Defaults],L1), Head1 =.. L1, add_ancestor_args(Body,[[],[],Defaults],Body1); %true -> Head =.. L, append(L,[PosAncestors,NegAncestors,Defaults],L1), Head1 =.. L1, add_ancestor_args(Body,[NewPosAncestors,NewNegAncestors,Defaults],Body2), (Body == Body2 -> Body1 = Body2; negative_literal(Head) -> NewPosAncestors = PosAncestors, conjoin((NewNegAncestors = [Head|NegAncestors]),Body2,Body1); %true -> NewNegAncestors = NegAncestors, conjoin((NewPosAncestors = [Head|PosAncestors]),Body2,Body1)). ancestor_tests(P,N,Result) :- P == query -> Result = true; P == gamma -> Head = gamma(DefaultID,DefaultConseq,_,_,Defaults), Default = gamma(DefaultID,DefaultConseq), Result = (Head :- identical_member(Default,Defaults), !, fail); P == alpha -> Result = true; % ??? <== Please, VERIFY ! %true -> negated_functor(P,NotP), N3 is N - 3, % N - 3 due to 3 ancestor-lists functor(Head1,P,N3), Head1 =.. [P|Args1], Head2 =.. [NotP|Args1], append(Args1,[PosAncestors,NegAncestors,_],Args), Head =.. [P|Args], (negative_functor(P) -> C1Ancestors = NegAncestors, C2Ancestors = PosAncestors; %true -> C1Ancestors = PosAncestors, C2Ancestors = NegAncestors), C1 = (Head :- identical_member(Head1,C1Ancestors), !, fail), count_inferences_pred(IncNcalls), (N3 = 0 -> % special case for propositional calculus conjoin((identical_member(Head2,C2Ancestors) , !),IncNcalls,V); %true -> conjoin(unifiable_member(Head2,C2Ancestors),IncNcalls,V)), (compile_proof_printing -> conjoin(V,infer_by(reduction(Head2)),V1); %true -> V1 = V), C2 = (Head :- V1), conjoin(C1,C2,Result). procedures_with_tests([[P,N]|Preds],Clauses,Procs) :- procedure(P,N,Clauses,Proc0), ancestor_tests(P,N,TestsA), lemma_tests(P,N,TestsL), conjoin(TestsA,TestsL,Tests), phook_tests(P,N,Tests,Proc0,ProcP), procedures_with_tests(Preds,Clauses,ProcsPs), conjoin(ProcP,ProcsPs,Procs). procedures_with_tests([],_Clauses,true). %%% Consistency checking. %%% %%% Add extra arguments to each goal so that information %%% on what assumptions were made in the proof can be checked %%% at each step/the end. %%% %%% I suppose Wff has to be replaced by cmm(Model,ModelStructure) ... %%% [all this is a quick copy of add_proof_recording ...] add_consistency_checking((Head :- Body),(Head1 :- Body1)) :- functor(Head,query,_) -> Head1 = Head, conjoin(model_initialization(MM0),Body,Body2), add_consistency_checking_args(Body2,MM0,MMOut,Body1); %true -> Head =.. L, append(L,[MMIn,MMOut],L1), Head1 =.. L1, add_consistency_checking_args(Body,MMIn,MMOut,Body1). add_consistency_checking_args(Body,MMIn,MMOut,Body1) :- Body = (A , B) -> add_consistency_checking_args(A,MMIn,MMIn1,A1), add_consistency_checking_args(B,MMIn1,MMOut,B1), conjoin(A1,B1,Body1); Body = (A ; B) -> add_consistency_checking_args(A,MMIn,MMOut,A1), add_consistency_checking_args(B,MMIn,MMOut,B1), disjoin(A1,B1,Body1); Body =.. [search,Goal|L] -> add_consistency_checking_args(Goal,MMIn,MMOut,Goal1), % ??? Body1 =.. [search,Goal1|L]; Body = justification(X) -> Body1 = compatible(X,MMIn,MMOut); Body = fail -> Body1 = Body; builtin(Body) -> MMIn = MMOut, Body1 = Body; %true -> Body =.. L, append(L,[MMIn,MMOut],L1), Body1 =.. L1. add_model_structure(WffI,Q,C,WffO) :- WffI = (A , B) -> add_model_structure(A,Q,C,A1), add_model_structure(B,Q,C,B1), conjoin(A1,B1,WffO); WffI = (A ; B) -> add_model_structure(A,Q,C,A1), add_model_structure(B,Q,C,B1), disjoin(A1,B1,WffO); WffI = (A :- B) -> add_model_structure(B,Q,C,B1), WffO = (A :- B1); WffI = model_initialization(Var) -> combine_clauses(Q,C,Matrix), WffO = model_initialization(Matrix,Var); %true -> WffO = WffI. classical_clauses(WffI,WffO) :- WffI = (A , B) -> classical_clauses(A,A1), classical_clauses(B,B1), conjoin(A1,B1,WffO); WffI = (A ; B) -> classical_clauses(A,A1), classical_clauses(B,B1), disjoin(A1,B1,WffO); WffI = (A :- B) -> % ??? (special case query elim. TS Apr04) WffO = true; builtin(WffI) -> WffO = true; %true -> WffI = WffO. query_clause(WffI,WffO) :- WffI = (A , B) -> (query_clause(A,WffO); query_clause(B,WffO)); WffI = (A ; B) -> (query_clause(A,WffO); query_clause(B,WffO)); WffI = (A :- B) -> (A = query -> classical_clauses(B,WffO); %true -> fail); %true -> fail. query(M) :- % call query with depth bound M (compile_complete_search, compile_proof_printing , lemma_handling_flag) -> query(M,_N,_LemProof,_LemProofEnd,_Proof,_ProofEnd); (compile_complete_search, (compile_proof_printing ; lemma_handling_flag)) -> query(M,_N,_Proof,_ProofEnd); compile_complete_search -> query(M,_N). query :- % unbounded search of query (compile_complete_search -> query(1000000); %true -> ((compile_proof_printing , lemma_handling_flag) -> query(_LemProof,_LemProofEnd,_Proof,_ProofEnd); (compile_proof_printing ; lemma_handling_flag) -> query(Proof,_ProofEnd); %true -> query)). %%% ---------------------------------------------------------------------- %%% XRay: THE ACTUAL COMPILATION PROCEDURES %%% xray(Name) :- read_kb(Name,KB), dpttp(Name,KB). dpttp(Name,X) :- time(dpttp1(X,Y:Z),'Compilation Phase I'), time(dpttp2(Name,Y:Z),'Compilation Phase II'), time(dpttp3(Name),'Compilation Phase III'). dpttp(X) :- Name = 'temp', dpttp(Name,X). dpttp1(X,Y:C) :- nl, write('XRay input formulas:'), apply_to_conjuncts(X,write_clause,_), nl, constants(X,H), (H = [] -> nl,write('Empty Herbrand universe.'),nl; %true -> nl,write('Herbrand universe':H),nl), classical_clauses(X,C0), cnf(C0,C1), make_matrix(C1,C2), instantiation(C2,H,C3), matrix_reduction(C3,C), (verbose_flag -> nl, write('Classical output formulas:'), apply_to_list(C,write_clause,_), nl; %true -> true), dpttp1(X,C,Y:C). dpttp1(X,C,Y:C) :- query_clause(X,Q0), variables(Q0,Vars), (Vars=[] -> cnf(Q0,Q1), make_matrix(Q1,Q2), matrix_reduction(Q2,Q), XQ=X; %true -> Q = [], apply_to_conjuncts(X,add_answer_preds,XQ)), (verbose_flag -> nl, write('Query formula:'), apply_to_conjuncts(Q0,write_clause,_), nl, write(' compiled:'), apply_to_list(Q,write_clause,_), nl,nl; %true -> true), dpttp1(XQ,Q,C,Y:C). dpttp1(X,Q,C,Y:C) :- clauses(X,XC,1), constants(X,H), (H = [] -> XH=true, X0=XC; %true -> herbrand_preds(H,XH), apply_to_conjuncts(XC,add_herbrand_preds,X0)), apply_to_conjuncts(X0,add_count_inferences,X1), apply_to_conjuncts(X1,add_ancestor,X2), predicates(X2,Preds0), reverse(Preds0,Preds), procedures_with_tests(Preds,X2,X3), /* all contrapositives available */ apply_to_conjuncts(X3,add_sound_unification,X4), apply_to_conjuncts(X4,add_consistency_checking,X5), (compile_complete_search -> apply_to_conjuncts(X5,add_complete_search,X6); %true -> X5=X6), apply_to_conjuncts(X6,add_lemmatization,XL), /* relies on 'infer_by */ (compile_proof_printing -> apply_to_conjuncts(XL,add_proof_recording,X7); %true -> X7 = XL), add_model_structure(X7,Q,C,X8), apply_to_conjuncts(X8,add_body_hooks,XD), apply_to_conjuncts(X,prolog_clause,XP), conjoin(XP,XD,XR), conjoin(XH,XR,Y), (verbose_flag -> nl, write('XRay output formulas:'), apply_to_conjuncts(Y,write_clause,_), nl; %true -> true), !. dpttp1(X) :- dpttp1(X,_). dpttp2(Name,Y:Z) :- nl, write('XRay writing compiled clauses ... '), write_ckb(Name,Y), write_cmm(Name,Z), write('done.'), !. dpttp2(Y:Z) :- Name = 'temp', dpttp2(Name,Y:Z). dpttp3(Name) :- nl, write('XRay compiling clauses ... '), compile_ckb(Name), write('done.'), nl, write('XRay compiling query ... '), compile_query(Name), write('done.'), nl, !. dpttp3 :- Name = 'temp', dpttp3(Name).