<div class="notebook"> <div class="nb-cell program" data-background="true" data-singleline="true" name="p7"> % swish helper :-style_check(-discontiguous). :-style_check(-singleton). :- use_rendering(mathjax). </div> <div class="nb-cell program" data-background="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). </div> <div class="nb-cell markdown" name="md1"> # Materialien zu Kapitel 4 </div> <div class="nb-cell markdown" name="md2"> ## From Models to Proofs </div> <div class="nb-cell markdown" name="md4"> Central predicates: </div> <div class="nb-cell program" data-background="true" name="p1"> tprove(F):- ( closedTableau([[f(F)]]), !, write('Theorem.'), nl ; write('Not a theorem.'), nl ). closedTableau([]). closedTableau(OldTableau):- expand(OldTableau,TempTableau), removeClosedBranches(TempTableau,NewTableau), closedTableau(NewTableau). </div> <div class="nb-cell markdown" name="md5"> Expanding tableau: </div> <div class="nb-cell program" data-background="true" name="p2"> expand([Branch|Tableau],[NewBranch|Tableau]):- unaryExpansion(Branch,NewBranch), !. expand([Branch|Tableau],[NewBranch|Tableau]):- conjunctiveExpansion(Branch,NewBranch), !. expand([Branch|Tableau],[NewBranch1,NewBranch2|Tableau]):- disjunctiveExpansion(Branch,NewBranch1,NewBranch2), !. expand([Branch|Rest],[Branch|Newrest]):- expand(Rest,Newrest). unaryExpansion(Branch,[Component|Temp]):- unary(SignedFormula,Component), removeFirst(SignedFormula,Branch,Temp). conjunctiveExpansion(Branch,[Comp1,Comp2|Temp]):- conjunctive(SignedFormula,Comp1,Comp2), removeFirst(SignedFormula,Branch,Temp). disjunctiveExpansion(Branch,[Comp1|Temp],[Comp2|Temp]):- disjunctive(SignedFormula,Comp1,Comp2), removeFirst(SignedFormula,Branch,Temp). 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)). 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)). unary(t(not(X)),f(X)). unary(f(not(X)),t(X)). </div> <div class="nb-cell query" name="q14"> expand([[f(or(a,b)),t(a)],[t(and(a,b))]],NewBranch). </div> <div class="nb-cell query" name="q15"> expand([[f(or(a,b)),t(not(a))],[t(and(a,b))]],NewBranch). </div> <div class="nb-cell query" name="q16"> expand([[t(or(a,b)),t(c)],[t(and(a,b))]],NewBranch). </div> <div class="nb-cell markdown" name="md17"> **Fragen:** * Warum ist es sinnvoll zuerst nach unaryExpansions zu suchen? * Warum ist es sinnvoll zuletzt nach disjunctiveExpansions zu suchen? </div> <div class="nb-cell markdown" name="md6"> Remove closed branches: </div> <div class="nb-cell program" data-background="true" name="p3"> removeClosedBranches([],[]). removeClosedBranches([Branch|Rest],Tableau):- closedBranch(Branch), !, removeClosedBranches(Rest,Tableau). removeClosedBranches([Branch|Rest],[Branch|Tableau]):- removeClosedBranches(Rest,Tableau). closedBranch(Branch):- memberList(t(X),Branch), memberList(f(X),Branch). </div> <div class="nb-cell query" name="q17"> trace,removeClosedBranches([[f(a),t(or(a,b)),t(a)],[t(not(a)),t(a)],[t(and(a,b)),f(and(a,b))]],Tableau). </div> <div class="nb-cell markdown" name="md12"> ### Examples Queries: </div> <div class="nb-cell query" name="q1"> write("Satz vom ausgeschlossenen Dritten: "), tprove(or(p,not(p))). </div> <div class="nb-cell query" name="q3"> write("Consequentia mirabilis: "), tprove(imp(imp(not(p),p),p)). </div> <div class="nb-cell query" name="q4"> write("Peircesches Gesetz: "), tprove(imp(imp(imp(p,q),p),p)). </div> <div class="nb-cell query" name="q2"> write("Implikation: "),tprove(or(not(p),q)). </div> <div class="nb-cell markdown" name="md18"> ### Try it yourself Load `propTableau.pl`and check that you understand the code. Have a look into `propTestSuite.pl` as well. Do the exercises below. </div> <div class="nb-cell markdown" name="md9"> ### Exercise 4.3.1: Try the prover out on some simple examples. Make sure you understand what is happening at each step. One way to do this is to use the standard Prolog `trace/O`, but a nicer way is to add the following code as a new second clause for the predicate closedTableau/1: `closedTableau(OldTableau):- nl,write(OldTableau),nl,fail.` Because this new clause always fails, it has no effect on the correctness of the predicate. However, before it fails it will write out the current state of the tableau, enabling you to follow the prover's progress easily. </div> <div class="nb-cell markdown" name="md10"> ### Exercise 4.3.2: Try to find examples of theorems which the tableau prover can't handle, or can't handle fast. That is, try to find propositional formulas which you know to be valid but which the tableau prover either won't halt on, or takes a long time to halt. (The last two formulas in the test suite are like this, but try to find your own examples before looking at these.) </div> <div class="nb-cell markdown" name="md13"> ### Exercise 4.3.3: Modify the code so that the tableau prover handles the bi-implication connective \( \leftrightarrow \) (use, say, `bimp/2` as the Prolog notation for this connective). </div> <div class="nb-cell markdown" name="md14"> ## Resolution </div> <div class="nb-cell markdown" name="md20"> ### Umwandlung einer Formel in Mengenklauselform </div> <div class="nb-cell markdown" name="md11"> **Formula to SetCNF:** </div> <div class="nb-cell program" data-background="true" name="p10"> % cnf.pl cnf(Formula,SetCNF):- nnf(Formula,NNF), nnf2cnf([[NNF]],[],CNF), setCnf(CNF,SetCNF). </div> <div class="nb-cell query" name="q5"> cnf(not(or(a,b)),CNF). </div> <div class="nb-cell query" name="q7"> cnf(not(and(a,b)),CNF). </div> <div class="nb-cell markdown" name="md3"> **Formula to NNF:** </div> <div class="nb-cell program" data-background="true" name="p4"> % cnf.pl 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). literal(not(F)):- atomic(F). literal(F):- atomic(F). </div> <div class="nb-cell query" name="q6"> nnf(not(and(a,b)),NNF). </div> <div class="nb-cell markdown" name="md7"> **NNF to CNF:** </div> <div class="nb-cell program" data-background="true" name="p5"> % cnf.pl nnf2cnf([],_,[]). nnf2cnf([[]|Tcon],Lit,[Lit|NewTcon]):- !, nnf2cnf(Tcon,[],NewTcon). nnf2cnf([[and(F1,F2)|Tdis]|Tcon],Lits,Output):- !, appendLists(Tdis,Lits,Full), nnf2cnf([[F1|Full],[F2|Full]|Tcon],[],Output). nnf2cnf([[or(F1,F2)|Tdis]|Tcon],Lits,Output):- !, nnf2cnf([[F1,F2|Tdis]|Tcon],Lits,Output). nnf2cnf([[Lit|Tdis]|Tcon],Lits,Output):- nnf2cnf([Tdis|Tcon],[Lit|Lits],Output). </div> <div class="nb-cell query" name="q12"> nnf2cnf([[or(and(c,d), not(b))]],[],CNF). </div> <div class="nb-cell query" name="q18"> nnf2cnf([[or(and(a,b),and(c,or(d,e)))]],[],CNF). </div> <div class="nb-cell markdown" name="md19"> Die schwierigste Klausel ist die, die in Zeile 9 beginnt. Überlege dir wofür `Tdis`, `Tcon` und `Lits` stehen könnte. Um zu sehen, wie `nnf2cnf/3` arbeitet, füge die Klausel `nnf2cnf(X,Y,Z):- nl, write(X), write(Y), write(Z),fail.` hinzu, die dir für jeden Schritt die einzelnen Argumentinstantiierungen ausgibt. </div> <div class="nb-cell markdown" name="md8"> **CNF to setCNF:** </div> <div class="nb-cell program" data-background="true" name="p6"> % cnf.pl setCnf(Cnf1,Cnf2):- setCnf(Cnf1,[],Cnf2). setCnf([],Cnf1,Cnf2):- removeDuplicates(Cnf1,Cnf2). setCnf([X1|L1],L2,L3):- removeDuplicates(X1,X2), setCnf(L1,[X2|L2],L3). </div> <div class="nb-cell query" name="q13"> setCnf([[not(b), not(a)]],SetCNF). </div> <div class="nb-cell query" name="q21"> trace, setCnf([[a,b,a,not(b)],[b,a,not(b)]],SetCNF). </div> <div class="nb-cell query" name="q19"> removeDuplicates([a,b,d,c,a,d,e,f],X). </div> <div class="nb-cell query" name="q20"> removeDuplicates([[a,b,c],[a,d,e],[c,b,a]],L). </div> <div class="nb-cell markdown" name="md21"> ### Implementierung der Resolutionsregel </div> <div class="nb-cell markdown" name="md15"> **main predicate** </div> <div class="nb-cell program" data-background="true" name="p8"> % propResolution.pl rprove(Formula):- cnf(not(Formula),CNF), refute(CNF). </div> <div class="nb-cell markdown" name="md22"> **Steuerung des Resolutionsprozesses** </div> <div class="nb-cell program" data-background="true" name="p11"> refute(C):- memberList([],C). refute(C):- \+ memberList([],C), resolveList(C,[],Output), unionSets(Output,C,NewC), \+ NewC = C, refute(NewC). resolveList([],Acc,Acc). resolveList([Clause|List],Acc1,Acc3):- resolveClauseList(List,Clause,Acc1,Acc2), resolveList(List,Acc2,Acc3). resolveClauseList([],_,Acc,Acc). resolveClauseList([H|L],Clause,Acc1,Acc3):- resolve(Clause,H,Result), unionSets([Result],Acc1,Acc2), resolveClauseList(L,Clause,Acc2,Acc3). resolveClauseList([H|L],Clause,Acc1,Acc2):- \+ resolve(Clause,H,_), resolveClauseList(L,Clause,Acc1,Acc2). </div> <div class="nb-cell query" name="q22"> </div> <div class="nb-cell markdown" name="md23"> **Resolutionsregel** </div> <div class="nb-cell program" name="p12"> resolve(Clause1,Clause2,NewClause):- selectFromList(Lit,Clause1,Temp1), selectFromList(not(Lit),Clause2,Temp2), unionSets(Temp1,Temp2,NewClause). resolve(Clause1,Clause2,NewClause):- selectFromList(not(Lit),Clause1,Temp1), selectFromList(Lit,Clause2,Temp2), unionSets(Temp1,Temp2,NewClause). </div> <div class="nb-cell query" name="q23"> resolve([p,s,not(t),r],[q,v,not(s),r],Result). </div> <div class="nb-cell markdown" name="md16"> ### Examples Queries: </div> <div class="nb-cell query" name="q8"> write("Satz vom ausgeschlossenen Dritten: "), rprove(or(p,not(p))). </div> <div class="nb-cell query" name="q10"> write("Consequentia mirabilis: "), rprove(imp(imp(not(p),p),p)). </div> <div class="nb-cell query" name="q11"> write("Peircesches Gesetz: "), rprove(imp(imp(imp(p,q),p),p)). </div> <div class="nb-cell query" name="q9"> write("Implikation: "),rprove(or(not(p),q)). </div> <div class="nb-cell markdown" name="md24"> Es ist wieder eine gute Idee, sich Zwischenschritte ausgeben zu lassen, um den Resolutionsprozess besser zu verstehen. Eine Möglichkeit ist es die Klausel `refute(C):- nl,write(C),nl,fail.` einzufügen. </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>