<div class="notebook"> <div class="nb-cell markdown" name="md1"> # Materialien zu Kapitel 1 ## Vokabulare Zunächst testen wir, ob ein Vokabular die Anforderungen an ein Vokabular erfüllt. Abhängig von dem gewählten Repräsentationsformat gibt es vier verschiedene Überprüfungsprädikate: </div> <div class="nb-cell program" name="p1"> % Prolog representation of a vocabulary (1) % is_vocab1([[love,2], [hate,2], [customer,1], [vincent,0], [honey_bunny,0]]). is_vocab1([]). is_vocab1([[A,N]|T]) :- atom(A), integer(N), N > -1, not(member([A,_],T)), is_vocab1(T). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Prolog representation of a vocabulary (2) % is_vocab2([(love,2), (hate,2), (customer,1), (vincent,0), (honey_bunny,0)]). is_vocab2([]). is_vocab2([(A,N)|T]) :- atom(A), integer(N), N > -1, not(member((A,_),T)), is_vocab2(T). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Prolog representation of a vocabulary (3) % is_vocab3([relation(love,2), relation(robber,1), constant(vincent), constant(mia)]). is_vocab3([]). is_vocab3([relation(A,N)|T]):- atom(A), integer(N), N > 0, not(member(relation(A,_),T)), not(member(constant(A),T)), is_vocab3(T). is_vocab3([constant(A)|T]):- atom(A), not(member(relation(A,_),T)), not(member(constant(A),T)), is_vocab3(T). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Prolog representation of a vocabulary (4) % is_vocab4([relation(love,2), relation(sad,1), constant(butch,0), constant(mia,0)]). is_vocab4([]). is_vocab4([relation(A,N)|T]):- atom(A), integer(N), N > 0, not(member(relation(A,_),T)), not(member(constant(A,_),T)), is_vocab4(T). is_vocab4([constant(A,0)|T]):- atom(A), not(member(relation(A,_),T)), not(member(constant(A,_),T)), is_vocab4(T). </div> <div class="nb-cell query" name="q1"> </div> <div class="nb-cell markdown" name="md2"> ## Implementierung eines Modellcheckers in Prolog </div> <div class="nb-cell markdown" name="md5"> Die folgenden Prädikate finden sich alle in `modelChecker1.pl` (siehe unten). </div> <div class="nb-cell markdown" name="md4"> ## Schritt 1: Repräsentation von Modellen in Prolog Wir wählen folgendes Repräsentationsformat für Modelle in Prolog: </div> <div class="nb-cell program" data-background="true" name="p2"> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Representing Models in Prolog % model(Domain,InterpretationFunctionF) model([d1,d2,d3,d4,d5], [f(O,jules,d1), f(O,vincent,d2), f(O,pumpkin,d3), f(O,honey_bunny,d4), f(O,yolanda,d5), f(1,customer,[d1,d2]), f(1,robber,[d3,d4]), f(2,love,[(d3,d4)])]). </div> <div class="nb-cell markdown" name="md6"> </div> <div class="nb-cell markdown" name="md7"> **Übung:** übertragen sie das folgende Modell in die Prolognotation: F2(MIA) = d2 F2(HONEY-BUNNY) = d1 F2(VINCENT) = d4 F2(YOLANDA) = d3 F2(CUSTOMER) = {d1,d2,d4} F2(RODBER) = {d3} F2(LOVE) = {}. **Programmierübung:** Schreiben sie ein Programm, das überprüft, ob ein Modell ein Modell in Prolognotation ist. </div> <div class="nb-cell program" name="p5"> % Lösung: isModel(model(Domain,[])):- isAtomList(Domain). isModel(model(Domain,[f(N,Function,Entity)|T])):- atom(Function), checkF(f(N,Function,Entity),Domain), not(member(f(_,Function,_),T)), isModel(model(Domain,T)). isAtomList([]). isAtomList([H|T]):- atom(H), isAtomList(T). checkF(f(0,_Function,Entity),D):- member(Entity,D). checkF(f(1,_Function,Entity),D):- sublist(Entity,D). checkF(f(2,_Function,Entity),D):- pairlist(Entity,D). sublist([],_L). sublist([H|T],L):- member(H,L), sublist(T,L). pairlist([],_L). pairlist([(A,B)|T],L):- member(A,L), member(B,L), pairlist(T,L). </div> <div class="nb-cell query" name="q3"> isModel(model([d1,d2,d3,d4,d5],[f(0,mia,d3),f(1,robber,[d2,d4,d5]),f(2,love,[(d2,d3),(d1,d4)])])). </div> <div class="nb-cell markdown" name="md8"> ## Schritt 2: Repräsentation von Formeln in Prolog Beispiele: Übertrage die Beispiele in Pädikatenlogik </div> <div class="nb-cell program" name="p4"> some(X,some(Y,love(X,Y))). not(all(X,all(Y,love(X,Y)))). all(X,or(robber(X),customer(X))). </div> <div class="nb-cell markdown" name="md10"> Übertrage die folgenden Formeln in die Prologrepräsentation: * ∃x robber(x) * ∀x ∃y ((robber(x) ∧ customer(y)) → love(x,y)) * ∀x (¬robber(x) ∨ customer(x)) </div> <div class="nb-cell markdown" name="md9"> ## Schritt 3: Implementierung der Satisfaction-Relation in Prolog </div> <div class="nb-cell program" name="p3"> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Implementation: Satisfaction in Prolog % taken from modelChecker1.pl by Patrick Blackburn und Johan Bos (slightly adapted) % satisfy/4 % statisfy(Formula,Model,Assignment,Polarity) %% complex formulas % not satisfy(not(Formula),Model,G,pos):- satisfy(Formula,Model,G,neg). satisfy(not(Formula),Model,G,neg):- satisfy(Formula,Model,G,pos). % and satisfy(and(Formula1,Formula2),Model,G,pos):- satisfy(Formula1,Model,G,pos), satisfy(Formula2,Model,G,pos). satisfy(and(Formula1,Formula2),Model,G,neg):- satisfy(Formula1,Model,G,neg); satisfy(Formula2,Model,G,neg). % or satisfy(or(Formula1,Formula2),Model,G,pos):- satisfy(Formula1,Model,G,pos); satisfy(Formula2,Model,G,pos). satisfy(or(Formula1,Formula2),Model,G,neg):- satisfy(Formula1,Model,G,neg), satisfy(Formula2,Model,G,neg). % imp satisfy(imp(Formula1,Formula2),Model,G,Pol):- satisfy(or(not(Formula1),Formula2),Model,G,Pol). % satisfy/4 % statisfy(Formula,Model,Assignment,Polarity) % quantifiers % some satisfy(some(X,Formula),model(D,F),G,pos):- memberList(V,D), % memberlist equals member and is defined in comSemPredicates.pl satisfy(Formula,model(D,F),[g(X,V)|G],pos). satisfy(some(X,Formula),model(D,F),G,neg):- setof(V,( memberList(V,D), satisfy(Formula,model(D,F),[g(X,V)|G],neg) ), Dom), setof(V,memberList(V,D),Dom). % all satisfy(all(X,Formula),Model,G,Pol):- satisfy(not(some(X,not(Formula))),Model,G,Pol). % satisfy/4 % statisfy(Formula,Model,Assignment,Polarity) %% atomic formulas % 1-place predicates satisfy(Formula,model(D,F),G,pos):- compose(Formula,Symbol,[Argument]), i(Argument,model(D,F),G,Value), memberList(f(1,Symbol,Values),F), memberList(Value,Values). satisfy(Formula,model(D,F),G,neg):- compose(Formula,Symbol, [Argument]), i(Argument,model(D,F),G,Value), memberList(f(1,Symbol,Values),F), \+ memberList(Value,Values). % 2-place predicates satisfy(Formula,model(D,F),G,pos):- compose(Formula,Symbol,[Arg1,Arg2]), i(Arg1,model(D,F),G,Value1), i(Arg2,model(D,F),G,Value2), memberList(f(2,Symbol,Values),F), memberList((Value1,Value2),Values). satisfy(Formula,model(D,F),G,neg):- compose(Formula,Symbol,[Arg1,Arg2]), i(Arg1,model(D,F),G,Value1), i(Arg2,model(D,F),G,Value2), memberList(f(2,Symbol,Values),F), \+ memberList((Value1,Value2),Values). % equality (2-place predicate with fixed interpretation) satisfy(eq(X,Y),Model,G,pos):- i(X,Model,G,Value1), i(Y,Model,G,Value2), Value1=Value2. satisfy(eq(X,Y),Model,G,neg):- i(X,Model,G,Value1), i(Y,Model,G,Value2), \+ Value1=Value2. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Assignment % i/4 % i(Variable,Model,Assignment,AssignedValue) i(X,model(_,F),G,Value):- ( var(X), memberList(g(Y,Value),G), Y==X, ! % IMPORTANT CUT! ; atom(X), memberList(f(0,X,Value),F) ). /*======================================================================== Auxiliary predicates: ========================================================================*/ % List membership (entspricht member) memberList(X,[X|_]). memberList(X,[_|Tail]):- memberList(X,Tail). % Zerlegung komplexer Terme (entspricht unif) compose(Term,Symbol,ArgList):- Term =.. [Symbol|ArgList]. </div> <div class="nb-cell query" name="q2"> </div> <div class="nb-cell markdown" name="md3"> **Aufgaben:** * Warum ist `satisfy`4-stellig? Wozu benötigen wir das `Polarity`-Argument? * Warum benötigen wir in der obigen Definition in Zeile 63 `setof(V,memberList(V,D),Dom)`, könnten wir nicht direkt mit `D` anstelle von `Dom` in den Zeilen darüber arbeiten? * Warum haben wir in der equality-Definition in Zeile 110 ` Value1=Value2` und nicht ` Value1==Value2`? * Überlege dir eine in dem Modell valide Formel und stelle eine Anfrage, die prüft, ob die Formel in dem Modell erfüllt wird. * Überlege dir eine in dem Modell invalide Formel und stelle eine Anfrage, die prüft, ob die Formel in dem Modell erfüllt wird. * Wie muss die Anfrage an `satisfy/4` lauten, um die Formel `some(X,and(customer(X),some(X,robber(X))))` in dem Modell zu evaluieren? Erkläre warum die Evaluation das gewünschte Ergebnis liefert und warum es zu keinem Problem kommt, obwohl die Variable `X` in zwei unterschiedlichen Bindungskontexten vorkommt. * Wenn man wissen möchte, welche Assignments die Anfrage `customer(X)` erfüllen, wie muss die Anfrage lauten? * Die Implementierung des Model-Checkers ist noch nicht perfekt. Welche Probleme treten auf? </div> <div class="nb-cell markdown" name="md11"> ## Verbesserung des ModelCheckers * Schreiben Sie ein Prädikat, das testet, ob eine Formel syntaktisch wohlgeformt ist und nur Prädikate und Konstanten verwendet, die in einem gegebenen Modell definiert sind. `syntaxCheck/2` mit `syntaxCheck(Formula,Model)` * Erweitern sie ihr Prädikat zu einem Prädikat `checkSentence/2`mit `checkSentence(Formula,Model)`, das gelingt, wenn die Formel syntaktisch wohlgeformt ist und keine freien Variablen enthält. **Lösung:** Im zip-File auf der Kurswebsite finden sie die Datei`modelChecker_wp.pl` mit diesen Prädikaten. Ziel von `modelChecker_wp.pl` war es, den ursprünglichen Model Checker `modelChecker1.pl` möglichst wenig zu verändern und den Evaluabilitätstest unabhängig von dem Test auf Erfüllung (satisfaction) durchzuführen. Effizienter ist es natürlich beides parallel zu tun, wie es in `modelChecker2.pl` umgesetzt wurde. </div> </div>