道歉是一种艺术

nullFortgeschrittene ProgrammierungFortgeschrittene ProgrammierungLuc De Raedt (original slides by Peter Flach)Meta-InterpreterMeta-InterpreterProlog meta-interpretersProlog meta-interpreters A meta-interpreter for a language is an interpreter for the language written in the language itself. /* solve(Goal) :- Goal is true given the pure Prolog program defined by clause/2. */ prove(true):-!. prove((A,B)):-!, prove(A), prove(B). prove(A):- /* not A=true, not A=(X,Y) */ clause(A,B), prove(B).p.70-2Meta-level vs. object-levelMeta-level vs. object-levelp.71Meta-interpreter computing proof treesMeta-interpreter computing proof trees /* solve(Goal,Tree) :- Tree is a proof tree for Goal given the program defined by clause/2. */ solve(true,true) :- !. solve((A,B),(ProofA,ProofB)) :- !, solve(A,ProofA), solve(B,ProofB). solve(A,(A:-builtin)) :- predicate_property(A, built_in), !, call(A). solve(A,(A:-Proof)) :- clause(A,B), solve(B,Proof).Meta-interpreter computing proof treesMeta-interpreter computing proof trees :-dynamic daughter/2 , father/2, son/2, male/1, female/1. father(abraham,isaac). male(isaac). father(haran,lot). male(lot). father(haran,milcah). female(milcah). father(haran,yiscah). female(yiscah). daughter(X,Y) :- father(Y,X), female(X). son(X,Y) :- father(Y,X), male(X). ?-solve(son(lot,X),P). P = (son(lot,haran):-(father(haran,lot):-true),(male(lot):-true)), X = haran ? Meta-interpreter with depth-limitMeta-interpreter with depth-limit /* solve(Goal, MaxDepth, Tree) :- Tree is a proof tree of MaxDepth for Goal given the program defined by clause/2. */ solve(true,D,true) :- D > 0, !. solve((A,B),D,(ProofA,ProofB)) :- D > 0, !, solve(A,D,ProofA), solve(B,D,ProofB). solve(A,D,(A:-Proof)) :- D > 0, clause(A,B), NewD is D - 1, solve(B,NewD,Proof). Simple tracer for pure PrologSimple tracer for pure Prolog /* trace(Goal) :- a simple tracer for pure Prolog, tracing the proof by side effects */ trace(true) :- !. trace((A,B)) :- !, trace(A), trace(B). trace(A) :- clause(A,B), write(A), trace(B). trace(A) :- \+ clause(A,B), write('No clause for '), write(A), nl, fail. A Theorem Prover for Full Clausal Logic: SATCHMOA Theorem Prover for Full Clausal Logic: SATCHMOSATCHMOSATCHMO(Full) clauses : h1;...;hn :- b1,...,bm h1 or ... or hn if b1 and ... and bm (Roughly) an interpretation is a set of (ground) facts We will restrict ourselves to Herbrand interpretations (interpretations using the constants, functors and predicates that occur in the theory) An interpretation M is a model for a clause c if and only if for all substitutions such that also SATCHMOSATCHMOIf M is not a model for c then c is a violated clause wrt M An interpretation M is a model for clausal theory (a set of clauses) if and only if it is a model for all clauses in the theory A clausal theory C is not satisfiable (inconsistent) C |=  if and only if there exists no model for C. Otherwise, it is satisfiable. Proof by refutation: if and only if  A model M is minimal for a theory T if no proper subset of M is a model of T.Give some model?Give some model? woman ; man :- human. human :- man. human :- woman. false :- man, woman. woman(X) ; man(X) :- human(X). human(X) :- man(X). human(X) :- woman(X). false :- man(X), woman(X). man(dracula).Give some model?Give some model? woman(X) ; man(X) :- human(X). human(X) :- man(X). human(X) :- woman(X). false :- man(X), woman(X). false :- human(X), bat(X). man(dracula). bat(dracula). Towards SATCHMO (Manthey and Bry, 1988) Towards SATCHMO (Manthey and Bry, 1988) initialize the current model M := {true} while possible do - search for a violated clause of which the body is in the current model M - add a literal from the head to the model if no clause is violated then M is a model Assumption: clauses are range-restricted (all variables in the head of a clause also appear in the body of the clause)  Towards SATCHMOTowards SATCHMOclauses: predicate cl/1 cl(( woman(X) ; man(X) :- human(X))) Models are represented by lists of facts Implementation of predicates: - satisfied_head(Head,Model) - satisfied_body(Body,Model)SATCHMO in PrologSATCHMO in Prolog% model(M) <- M is a model of the clauses defined by cl/1 model(M):- model([],M). model(M0,M):- is_violated(Head,M0),!, % instance of violated clause disj_element(L,Head), % L: ground literal from head model([L|M0],M). % add L to the model model(M,M). % no more violated clauses is_violated(H,M):- cl((H:-B)), satisfied_body(B,M), % grounds the variables not satisfied_head(H,M).p.111SATCHMO in PrologSATCHMO in Prologsatisfied_body(true,M). satisfied_body(A,M) :- member(A,M). satisfied_body((A,B),M) :- member(A,M), satisfied_body(B,M). satisfied_head(A,M) :- member(A,M). satisfied_head((A;B), M) :- member(A,M). satisfied_head((A;B), M) :- satisfied_head(B, M).SATCHMO in PrologSATCHMO in Prolog disj_element(X,X) :- \+ X = false, \+ X = (One;TheOther). disj_element(X,(X;Ys)). disj_element(X,(Y;Ys)) :- disj_element(X, Ys).  cl(((woman(X);man(X)) :- human(X))). cl((human(X) :- man(X))). cl((human(X) :- woman(X))). cl((false :- man(X), woman(X))). cl((false :- human(X), bat(X))). % cl((man(dracula) :- true)). cl((bat(dracula) :- true)).   Forward chaining: exampleForward chaining: examplemarried(X);bachelor(X):-man(X),adult(X). has_wife(X):-married(X),man(X). man(paul). adult(paul).?-model([],M)