<div class="notebook open-fullscreen">

<div class="nb-cell program" name="p10">
% Auszug aus modelChecker1.pl
% 
% adapted by Wiebke Petersen
</div>

<div class="nb-cell markdown" name="md1">
# Solving the Querying Task in Prolog
</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="md2">
Schreibe ein Prädikat isModel/1, das prüft, ob etwas ein Modell im obigen Format ist.
</div>

<div class="nb-cell program" data-singleline="true" 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 markdown" name="md8">
## Schritt 2: Repräsentation von Formeln in Prolog

Wir wählen folgendes Repräsentationsformat für Formeln in Prolog:
</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="md9">
## Schritt 3: Implementierung der Satisfaction-Relation in Prolog
</div>

<div class="nb-cell markdown" name="md5">
Der folgende Code stammt aus modelChecker1.pl von Patrick Blackburn und Johan Bos.
</div>

<div class="nb-cell program" data-background="true" name="p7">
% satisfy/4
% statisfy(Formula,Model,Assignment,Polarity)
</div>

<div class="nb-cell program" data-background="true" data-singleline="true" name="p3">
% satisfy/4 - 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).
</div>

<div class="nb-cell program" data-background="true" data-singleline="true" name="p1">
% satisfy/4 - 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).
</div>

<div class="nb-cell program" data-background="true" data-singleline="true" name="p6">
% satisfy/4 - 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.
</div>

<div class="nb-cell program" data-background="true" data-singleline="true" name="p8">
% Assignment i/4

% 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)
   ).
</div>

<div class="nb-cell markdown" name="md6">
Die Hilfsprädikate, die immer wieder benötigt werden sind in comsemPredicates.pl ausgelagert. Hier werden auch einige vordefinierte Prologprädikate definiert, um eine Anpassung an andere Prologdialekte zu vereinfachen.
</div>

<div class="nb-cell program" data-background="true" data-singleline="true" name="p9">
% Auxiliary predicates: (entnommen aus comsemPredicates.pl)

% 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">
model(D,F),
satisfy(some(X,and(customer(X),some(X,robber(X)))),model(D,F),[],pos).
</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>