<div class="notebook"> <div class="nb-cell program" data-background="true" data-singleline="true" name="p7"> % swish helper :-style_check(-discontiguous). :-style_check(-singleton). </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p9"> % consemPredicates (excerpt) /*======================================================================== List membership ========================================================================*/ memberList(X,[X|_]). memberList(X,[_|Tail]):- memberList(X,Tail). /*======================================================================== Removing first member of a list ========================================================================*/ removeFirst(X,[X|Tail],Tail) :- !. removeFirst(X,[Head|Tail],[Head|NewTail]):- removeFirst(X,Tail,NewTail). /*======================================================================== Appending two lists ========================================================================*/ appendLists([],List,List). appendLists([X|Tail1],List,[X|Tail2]):- appendLists(Tail1,List,Tail2). /*======================================================================== Remove Duplicates ========================================================================*/ removeDuplicates([],[]). removeDuplicates([X|L],Pruned):- memberList(Y,L), X==Y, !, removeDuplicates(L,Pruned). removeDuplicates([X|L],[X|Pruned]):- removeDuplicates(L,Pruned). /*======================================================================== Selecting (i.e. removing) a member of a list ========================================================================*/ selectFromList(X,[X|L],L). selectFromList(X,[Y|L1],[Y|L2]):- selectFromList(X,L1,L2). /*======================================================================== Union of two sets (disallowing unification of list elements) ========================================================================*/ unionSets([],L,L). unionSets([X|L1],L2,L3):- memberList(Y,L2), X==Y, !, unionSets(L1,L2,L3). unionSets([X|L1],L2,[X|L3]):- unionSets(L1,L2,L3). /*======================================================================== Substitution Predicates ========================================================================*/ substitute(Term,Var,Exp,Result):- Exp==Var, !, Result=Term. substitute(_Term,_Var,Exp,Result):- \+ compound(Exp), !, Result=Exp. substitute(Term,Var,Formula,Result):- compose(Formula,Functor,[Exp,F]), memberList(Functor,[lam,all,some]), !, ( Exp==Var, !, Result=Formula ; substitute(Term,Var,F,R), compose(Result,Functor,[Exp,R]) ). substitute(Term,Var,Formula,Result):- compose(Formula,Functor,ArgList), substituteList(Term,Var,ArgList,ResultList), compose(Result,Functor,ResultList). substituteList(_Term,_Var,[],[]). substituteList(Term,Var,[Exp|Others],[Result|ResultOthers]):- substitute(Term,Var,Exp,Result), substituteList(Term,Var,Others,ResultOthers). /*======================================================================== Skolem Function Counter ========================================================================*/ :- dynamic(functionCounter/1). functionCounter(1). newFunctionCounter(N):- functionCounter(N), M is N+1, retract(functionCounter(N)), asserta(functionCounter(M)). /*======================================================================== Basic Formula Syntax ========================================================================*/ basicFormula(F):- var(F), !, fail. basicFormula(F):- compose(F,Symbol,Args), \+ memberList(Symbol,[not,and,imp,app,or,some,all,lam,eq]), simpleTerms(Args). /*======================================================================== Simple Terms ========================================================================*/ simpleTerms([]). simpleTerms([X|Rest]):- simpleTerm(X), simpleTerms(Rest). simpleTerm(T):- var(T); atomic(T); nonvar(T), functor(T,'$VAR',1); nonvar(T), functor(T,fun,_). /*======================================================================== Compose predicate argument structure ========================================================================*/ compose(Term,Symbol,ArgList):- Term =.. [Symbol|ArgList]. </div> <div class="nb-cell markdown" name="md1"> # Materialien zu Kapitel 5 </div> <div class="nb-cell markdown" name="md2"> ## Free Variable Tableaux </div> <div class="nb-cell markdown" name="md4"> Der folgende Code ist in freeVarTabl.pl. Lediglich die Reihenfolge der Prädikate wurde verändert: </div> <div class="nb-cell program" data-background="true" name="p1"> /*======================================================================== Try to create a tableau expansion for f(X) that is closed allowing Qdepth applications of the universal rule. ========================================================================*/ tprove(X,Qdepth):- notatedFormula(NotatedFormula,[],f(X)), closedTableau([[NotatedFormula]],Qdepth). /*======================================================================== Notate the free variables of a formula ========================================================================*/ notatedFormula(n(Free,Formula),Free,Formula). </div> <div class="nb-cell markdown" name="md5"> Für jede Formel wird explizit die Liste der freien Variablen angegeben (notatedFormula). Statt mit einer Formel wie love(X,Y) arbeiten wir mit der notated Formel n([X,Y],love(X,Y)). </div> <div class="nb-cell query" name="q11"> notatedFormula(NF,[X,Y],love(X,Y)). </div> <div class="nb-cell markdown" name="md27"> Der Zähler Qdepth kontrolliert, wie oft eine universal rule angewandt werden darf. Ein solcher Zähler ist notwendig, um den kontrollierten Abbruch zu erzwingen, da die Prädikatenlogik nicht entscheidbar ist. Bei einem Abbruch wissen wir aber nicht, ob kein Beweis für die Gültigkeit einer Formel existiert, oder ob wir nur noch keinen gefunden haben. **Aufgabe:** Erkläre die Antworten auf die folgenden Anfragen: </div> <div class="nb-cell query" name="q3"> tprove(some(X,or(p(X),not(p(X)))),100). </div> <div class="nb-cell query" name="q4"> tprove(all(X,or(p(X),not(p(X)))),100). </div> <div class="nb-cell query" name="q5"> tprove(some(X,or(p(X),not(p(X)))),0). </div> <div class="nb-cell query" name="q10"> tprove(all(X,or(p(X),not(p(X)))),0). </div> <div class="nb-cell markdown" name="md28"> Der folgende Code zur Übrprüfung, ob ein Tableau geschlossen ist, unterscheidet sich kaum von der Tableau-Implementierung für die Aussagenlogik: </div> <div class="nb-cell program" data-background="true" name="p2"> /*======================================================================== Expand Tableau until it is closed, allowing Qdepth applications of the universal rule. ========================================================================*/ closedTableau([],_Q):- !. closedTableau(OldTableau,Qdepth):- expand(OldTableau,Qdepth,TempTableau,NewQdepth), !, removeClosedBranches(TempTableau,NewTableau), %write("Qdepth: "),write(NewQdepth),tab(3),write("tableau: "),write(NewTableau),nl, % Ausgabe von Zaehler und Tableau closedTableau(NewTableau,NewQdepth). /*======================================================================== Remove all closed branches ========================================================================*/ removeClosedBranches([],[]). removeClosedBranches([Branch|Rest],Tableau):- closedBranch(Branch), !, removeClosedBranches(Rest,Tableau). removeClosedBranches([Branch|Rest],[Branch|Tableau]):- removeClosedBranches(Rest,Tableau). /*======================================================================== Check whether a branch is closed ========================================================================*/ closedBranch(Branch):- memberList(n(_,t(X)),Branch), memberList(n(_,f(Y)),Branch), basicFormula(X), basicFormula(Y), unify_with_occurs_check(X,Y). </div> <div class="nb-cell query" name="q6"> removeClosedBranches([[n([X],f(p(X))),n([],t(or(p(a),q(b)))),n([],t(p(a)))],[n([Y],t(not(p(Y)))),n([],t(p(a)))],[n([],t(and(p(a),q(b)))),n([],f(and(p(a),q(b))))]],Tableau). </div> <div class="nb-cell markdown" name="md17"> basicFormula/1 ist in comsemPredicates.pl definiert und überprüft, ob eine Formel ein Basisausdruck der Form p(t1,...,tn) ist, wobei p keine logische Konstante ist und alle ti simple Terme sind. Teste: ?- basicFormula(imp(a,b)), ?- basicFormula(love(a,X)), ?- basicFormula(X), ?- basicFormula(love(a,father(X))). </div> <div class="nb-cell query" name="q12"> basicFormula(love(a,X)). </div> <div class="nb-cell markdown" name="md29"> Die folgenden Zeilen zu den Expansionsschritten sind wieder völlig analog zu der Implementierung für die Aussagenlogik: </div> <div class="nb-cell program" data-background="true" name="p3"> /*======================================================================== Newtableau with Q-depth NewQdepth is the result of applying a tableau expansion rule to Oldtableau with a Q-depth of OldQdepth. ========================================================================*/ expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):- unaryExpansion(Branch,NewBranch). expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):- conjunctiveExpansion(Branch,NewBranch). expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):- existentialExpansion(Branch,NewBranch). expand([Branch|Tableau],QD,[NewBranch1,NewBranch2|Tableau],QD):- disjunctiveExpansion(Branch,NewBranch1,NewBranch2). % da universalExpansions mehrfach auf dieselbe Formel angewandt werden kann, % schieben wir die Formeln immer wieder nach hinten im Tableau % (sonst droht frühzeitiges Aufbrauchen des universellen Expansionsguthabens): expand([Branch|Tableau],OldQD,NewTableau,NewQD):- universalExpansion(Branch,OldQD,NewBranch,NewQD), appendLists(Tableau,[NewBranch],NewTableau). expand([Branch|Rest],OldQD,[Branch|Newrest],NewQD):- expand(Rest,OldQD,Newrest,NewQD). /*======================================================================== Take Branch as input, and return NewBranches if a tableau rule allows unary expansion. ========================================================================*/ unaryExpansion(Branch,[NotatedComponent|Temp]) :- unary(SignedFormula,Component), notatedFormula(NotatedFormula,Free,SignedFormula), removeFirst(NotatedFormula,Branch,Temp), notatedFormula(NotatedComponent,Free,Component). /*======================================================================== Take Branch as input, and return the NewBranch if a tableau rule allows conjunctive expansion. ========================================================================*/ conjunctiveExpansion(Branch,[NotatedComp1,NotatedComp2|Temp]):- conjunctive(SignedFormula,Comp1,Comp2), notatedFormula(NotatedFormula,Free,SignedFormula), removeFirst(NotatedFormula,Branch,Temp), notatedFormula(NotatedComp1,Free,Comp1), notatedFormula(NotatedComp2,Free,Comp2). /*======================================================================== Take Branch as input, and return the NewBranch1 and NewBranch2 if a tableau rule allows disjunctive expansion. ========================================================================*/ disjunctiveExpansion(Branch,[NotComp1|Temp],[NotComp2|Temp]):- disjunctive(SignedFormula,Comp1,Comp2), notatedFormula(NotatedFormula,Free,SignedFormula), removeFirst(NotatedFormula,Branch,Temp), notatedFormula(NotComp1,Free,Comp1), notatedFormula(NotComp2,Free,Comp2). /*======================================================================== Take Branch as input, and return the NewBranch if a tableau rule allows existential expansion. ========================================================================*/ existentialExpansion(Branch,[NotatedInstance|Temp]):- notatedFormula(NotatedFormula,Free,SignedFormula), existential(SignedFormula), removeFirst(NotatedFormula,Branch,Temp), skolemFunction(Free,Term), instance(SignedFormula,Term,Instance), notatedFormula(NotatedInstance,Free,Instance). </div> <div class="nb-cell markdown" name="md3"> Das Prädikat existentialExpansion/2 greift auf das Prädikat skolemFunction/2 zu, das einen neuen Skolemterm zu einer Liste von freien Variablen generiert: </div> <div class="nb-cell program" data-background="true" name="p4"> /*======================================================================== VarList is a list of free variables, and SkolemTerm is a previously unused Skolem function symbol fun(N) applied to those free variables. ========================================================================*/ % Teste mit '?- freeVarTabl:skolemFunction([X,Y,Z],S)' skolemFunction(VarList,SkolemTerm):- newFunctionCounter(N), compose(SkolemTerm,fun,[N|VarList]). </div> <div class="nb-cell query" name="q2"> skolemFunction([X,Y],ST). </div> <div class="nb-cell markdown" name="md6"> Weiter geht es mit der universalExpansion. Hier wird bei jedem Aufruf der Zähler QDepth um eins runtergesetzt. </div> <div class="nb-cell program" data-background="true" name="p5"> /*======================================================================== Take Branch and OldQD as input, and return the NewBranch and NewQDepthif a tableau rule allow universal expansion. ========================================================================*/ universalExpansion(Branch,OldQD,NewBranch,NewQD):- OldQD > 0, NewQD is OldQD - 1, memberList(NotatedFormula,Branch), notatedFormula(NotatedFormula,Free,SignedFormula), universal(SignedFormula), removeFirst(NotatedFormula,Branch,Temp), instance(SignedFormula,V,Instance), notatedFormula(NotatedInstance,[V|Free],Instance), appendLists([NotatedInstance|Temp],[NotatedFormula],NewBranch). </div> <div class="nb-cell markdown" name="md7"> Das Prädikat universalExpansion/2 ruft das Prädikat instance/3 auf (substitute/4 ist in comsemPred.pl` definiert): </div> <div class="nb-cell program" data-background="true" name="p6"> /*======================================================================== Remove quantifier from signed quantified formula, and replacing all free occurrences of the quantified variable by occurrences of Term. ========================================================================*/ % ?- freeVarTabl:instance(t(all(X,love(X,vincent))),Y,F). instance(t(all(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF). instance(f(some(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF). instance(t(some(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF). instance(f(all(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF). </div> <div class="nb-cell markdown" name="md8"> Der Rest ist analog zur Implementierung der Aussagenlogik: </div> <div class="nb-cell program" data-background="true" name="p8"> /*======================================================================== Decompose conjunctive signed formula ========================================================================*/ conjunctive(t(and(X,Y)),t(X),t(Y)). conjunctive(f(or(X,Y)),f(X),f(Y)). conjunctive(f(imp(X,Y)),t(X),f(Y)). /*======================================================================== Decompose disjunctive signed formula ========================================================================*/ disjunctive(f(and(X,Y)),f(X),f(Y)). disjunctive(t(or(X,Y)),t(X),t(Y)). disjunctive(t(imp(X,Y)),f(X),t(Y)). /*======================================================================== Decompose unary signed formula ========================================================================*/ unary(t(not(X)),f(X)). unary(f(not(X)),t(X)). /*======================================================================== Universal Signed Formulas ========================================================================*/ universal(t(all(_,_))). universal(f(some(_,_))). /*======================================================================== Existential Signed Formulas ========================================================================*/ existential(t(some(_,_))). existential(f(all(_,_))). </div> <div class="nb-cell markdown" name="md30"> **Aufgabe:** Kommentiere oben in `closedTableau/2` in Zeile 11, die `write`-Anweisungen ein, die die Zwischentableaus und den Zählerstand ausgeben und stelle die folgenden Anfragen. Was bedeutet es, wenn `tprove` scheitert (`false`)? </div> <div class="nb-cell query" name="q13"> tprove(some(X,snort(X)),3). </div> <div class="nb-cell query" name="q14"> tprove(imp(all(_488,all(_494,and(p(_488),p(_494)))),some(_488,some(_494,or(p(_488),p(_494))))),3). </div> <div class="nb-cell markdown" name="md31"> Setze in den beiden obigen Anfragen den Zähler auf 10 hoch und vergleiche die Antworten. </div> <div class="nb-cell markdown" name="md9"> ## Implementing FOL Resolution </div> <div class="nb-cell markdown" name="md10"> FOL in CNF umwandeln: </div> <div class="nb-cell program" data-background="true" name="p10"> cnf(Formula,SetCNF):- nnf(Formula,NNF), skolemise(NNF,Skolemised,[]), cnf([[Skolemised]],[],CNF), setCnf(CNF,SetCNF). </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p20"> % helper: skolemise /*======================================================================== Skolemise ========================================================================*/ skolemise(all(X,F),N,Vars):- skolemise(F,N,[X|Vars]). skolemise(some(X,F1),N,Vars):- skolemFunction(Vars,SkolemTerm), substitute(SkolemTerm,X,F1,F2), skolemise(F2,N,Vars). skolemise(and(F1,F2),and(N1,N2),Vars):- skolemise(F1,N1,Vars), skolemise(F2,N2,Vars). skolemise(or(F1,F2),or(N1,N2),Vars):- skolemise(F1,N1,Vars), skolemise(F2,N2,Vars). skolemise(F,F,_):- literal(F). /*======================================================================== Literals ========================================================================*/ literal(not(F)):- basicFormula(F). literal(F):- basicFormula(F). /*======================================================================== VarList is a list of free variables, and SkolemTerm is a previously unused Skolem function symbol fun(N) applied to those free variables. ========================================================================*/ skolemFunction(VarList,SkolemTerm):- newFunctionCounter(N), compose(SkolemTerm,fun,[N|VarList]). </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p18"> % helper: nnf to cnf /*======================================================================== Convert From Negative Normal Form to Conjunctive Normal Form ========================================================================*/ cnf([],_,[]). cnf([[]|Tcon],Lit,[Lit|NewTcon]):- !, cnf(Tcon,[],NewTcon). cnf([[and(F1,F2)|Tdis]|Tcon],Lits,Output):- !, appendLists(Tdis,Lits,Full), cnf([[F1|Full],[F2|Full]|Tcon],[],Output). cnf([[or(F1,F2)|Tdis]|Tcon],Lits,Output):- !, cnf([[F1,F2|Tdis]|Tcon],Lits,Output). cnf([[Lit|Tdis]|Tcon],Lits,Output):- cnf([Tdis|Tcon],[Lit|Lits],Output). /*======================================================================== Remove Duplicates and Sort ========================================================================*/ setCnf(Cnf1,Cnf2):- setCnf(Cnf1,[],Cnf2). setCnf([],Cnf1,Cnf2):- removeDuplicates(Cnf1,Cnf2). setCnf([X1|L1],L2,L3):- removeDuplicates(X1,X2), sort(X2,X3), setCnf(L1,[X3|L2],L3). </div> <div class="nb-cell markdown" name="md11"> Abweichungen zur Aussagenlogik (nnf) </div> <div class="nb-cell program" data-background="true" name="p11"> nnf(not(all(X,F)),some(X,N)):- nnf(not(F),N). nnf(all(X,F),all(X,N)):- nnf(F,N). nnf(not(some(X,F)),all(X,N)):- nnf(not(F),N). nnf(some(X,F),some(X,N)):- nnf(F,N). </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p14"> % remaining nnf nnf(not(and(F1,F2)),or(N1,N2)):- nnf(not(F1),N1), nnf(not(F2),N2). nnf(and(F1,F2),and(N1,N2)):- nnf(F1,N1), nnf(F2,N2). nnf(not(or(F1,F2)),and(N1,N2)):- nnf(not(F1),N1), nnf(not(F2),N2). nnf(or(F1,F2),or(N1,N2)):- nnf(F1,N1), nnf(F2,N2). nnf(not(imp(F1,F2)),and(N1,N2)):- nnf(F1,N1), nnf(not(F2),N2). nnf(imp(F1,F2),or(N1,N2)):- nnf(not(F1),N1), nnf(F2,N2). nnf(not(not(F1)),N1):- nnf(F1,N1). nnf(F1,F1):- literal(F1). /*======================================================================== Literals ========================================================================*/ literal(not(F)):- basicFormula(F). literal(F):- basicFormula(F). </div> <div class="nb-cell markdown" name="md12"> Resolution </div> <div class="nb-cell program" data-background="true" name="p12"> rprove(Formula):- cnf(not(Formula),CNF), nonRedundantFactors(CNF,NRF), refute(NRF). rprove(Formula,Result):- cnf(not(Formula),CNF), nonRedundantFactors(CNF,NRF), ( refute(NRF), !, Result = 'theorem' ; Result = 'not a theorem' ). </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p19"> % helper: refute /*======================================================================== Refute ========================================================================*/ refute(C):- memberList([],C). refute(C):- \+ memberList([],C), resolveList(C,[],Output), unionSets(Output,C,NewC), \+ NewC == C, refute(NewC). /*======================================================================== Resolve a list against a list ========================================================================*/ resolveList([],Acc,Acc). resolveList([Clause|List],Acc1,Acc3):- resolveClauseList(List,Clause,Acc1,Acc2), resolveList(List,Acc2,Acc3). /*======================================================================== Resolve a clause against a list ========================================================================*/ resolveClauseList([],_,Acc,Acc). resolveClauseList([H|L],Clause,Acc,Output):- resolve(Clause,H,Result0), nonRedundantFactors([Result0],Result), unionSets(Result,Acc,NewAcc), resolveClauseList(L,Clause,NewAcc,Output). resolveClauseList([H|L],Clause,Acc1,Acc2):- \+ resolve(Clause,H,_), resolveClauseList(L,Clause,Acc1,Acc2). </div> <div class="nb-cell markdown" name="md13"> Abweichungen und Erweiterungen </div> <div class="nb-cell program" data-background="true" name="p13"> /*======================================================================== Resolve two clauses ========================================================================*/ resolve(Clause1,Clause2,NewClause):- selectFromList(Lit1,Clause1,Temp1), selectFromList(not(Lit2),Clause2,Temp2), unify_with_occurs_check(Lit1,Lit2), unionSets(Temp1,Temp2,NewClause). resolve(Clause1,Clause2,NewClause):- selectFromList(not(Lit1),Clause1,Temp1), selectFromList(Lit2,Clause2,Temp2), unify_with_occurs_check(Lit1,Lit2), unionSets(Temp1,Temp2,NewClause). /*======================================================================== Compute Non-Redundant Factors for a list of clauses ========================================================================*/ nonRedundantFactors([],[]). nonRedundantFactors([C1|L1],L4):- findall(C2,nonRedFact(C1,C2),L3), nonRedundantFactors(L1,L2), appendLists(L3,L2,L4). /*======================================================================== Compute Non-Redundant Factors for a Clause ========================================================================*/ nonRedFact([],[]). nonRedFact([X|C1],C2):- memberList(Y,C1), unify_with_occurs_check(X,Y), nonRedFact(C1,C2). nonRedFact([X|C1],[X|C2]):- nonRedFact(C1,C2). </div> <div class="nb-cell markdown" name="md18"> ### Testanfragen: </div> <div class="nb-cell query" name="q7"> write("Theorem?"), rprove(all(X,or(p(X),not(p(X)))), Result). </div> <div class="nb-cell query" name="q8"> write("Theorem?"), rprove(imp(all(X,p(X)),not(some(Y,not(p(Y))))), Result). </div> <div class="nb-cell query" name="q1"> write("Theorem?"), rprove(some(X,or(p(X),q(X))), Result). </div> <div class="nb-cell query" name="q9"> write("Theorem?"), rprove(some(X,and(man(X),some(Y,woman(Y)))), Result). </div> <div class="nb-cell markdown" name="md14"> ## Off-the-Shelf Theorem Provers </div> <div class="nb-cell markdown" name="md16"> **Die folgenden Anfragen können innerhalb dieses SWISH Instanz nicht erfolgreich ausgeführt werden, da externe Skripte benötigt werden. Ab hier kommt nun die Virtual Box zum Einsatz.** Weitere Infos unter: https://user.phil.hhu.de/~petersen/SoSe20_CompSem/SoSe20_CompSem.html#vm </div> <div class="nb-cell markdown" name="md19"> ```prolog EQ = and(and(all(X,gleich(X,X)),all(X,forall(Y,imp(gleich(X,Y),gleich(Y,X))))),all(X,all(Y,all(Z,imp(and(gleich(X,Y),gleich(Y,Z)),gleich(X,Z)))))), Kontext = and(all(X,imp(woman(X),snort(X))),some(X,and(woman(X),gleich(mia,X)))), New = not(snort(mia)), rprove(imp(and(EQ,Kontext),not(New))). ``` </div> <div class="nb-cell markdown" name="md20"> ```prolog fol2otter(imp(all(X,dance(X)),not(some(Y,not(dance(Y))))),user). ``` </div> <div class="nb-cell markdown" name="md21"> ```prolog set(auto). assign(max_seconds,30). clear(print_proofs). set(prolog_style_variables). formula_list(usable). ((all A dance(A)) -> -((exists B -(dance(B))))). end_of_list. ``` </div> <div class="nb-cell markdown" name="md22"> ```prolog callTP(imp(all(X,dance(X)),not(some(Y,not(dance(Y))))),P,E). ``` </div> <div class="nb-cell markdown" name="md15"> ## Off-the-Shelf Model Builder </div> <div class="nb-cell markdown" name="md23"> ```prolog fol2mace(and(all(X,imp(boxer(X),slow(X))),and(boxer(butch),likes(mia,butch))),user). ``` </div> <div class="nb-cell markdown" name="md24"> ```prolog set(auto). clear(print_proofs). set(prolog_style_variables). formula_list(usable). ((all A (boxer(A) -> slow(A))) & (boxer(butch) & likes(mia,butch))). end_of_list. ``` </div> <div class="nb-cell markdown" name="md25"> ```prolog % callMB/4 % callMB(Problem,DomainSize, Model, ModelBuilder). callMB(and(all(X,imp(boxer(X),slow(X))),and(boxer(butch),likes(mia,butch))),5,Model,MB). ``` </div> <div class="nb-cell markdown" name="md26"> ```prolog Model = D=[d1] f(1,boxer,[d1]) f(1,slow,[d1]) f(0,butch,d1) f(0,mia,d1) f(2,likes,[(d1,d1)]) , MB = mace. ``` </div> <div class="nb-cell html" name="htm1"> <hr> <p style="color:#aaa">Mathjax Loader</p> <script> (function() { var nb = notebook; require(["https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js"+ "?config=TeX-MML-AM_CHTML"], function() { nb.markdown_post_renderer(function() { MathJax.Hub.Queue(["Typeset",MathJax.Hub,this[0]]); }); }); })(); </script> </div> </div>