<div class="notebook hide-navbar open-fullscreen">
<div class="nb-cell program" name="p9">
% Auszug aus cnf.pl
%
% adapted by Wiebke Petersen
</div>
<div class="nb-cell program" data-background="true" data-singleline="true" name="p5">
% 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">
### Formula to SetCNF
</div>
<div class="nb-cell program" data-background="true" name="p1">
% cnf.pl
cnf(Formula,SetCNF):-
nnf(Formula,NNF),
nnf2cnf([[NNF]],[],CNF),
setCnf(CNF,SetCNF).
</div>
<div class="nb-cell query" name="q1">
cnf(not(or(a,b)),CNF).
</div>
<div class="nb-cell query" name="q2">
cnf(not(and(a,b)),CNF).
</div>
<div class="nb-cell markdown" name="md2">
### Formula to NNF
* Schreibe $$\neg (\phi \land \psi)$$ um zu $$\neg \phi \lor \neg \psi$$
---
* Schreibe $$\neg (\phi \lor \psi)$$ um zu $$\neg \phi \land \neg \psi$$
---
* Schreibe $$\neg (\phi \rightarrow \psi)$$ um zu $$ \phi \land \neg \psi$$
---
* Schreibe $$(\phi \rightarrow \psi)$$ um zu $$\neg \phi \lor \psi$$
---
* Schreibe $$\neg \neg \phi$$ um zu $$\psi$$
</div>
<div class="nb-cell program" data-background="true" name="p2">
% 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="q3">
nnf(not(and(a,b)),NNF).
</div>
<div class="nb-cell markdown" name="md3">
### NNF to CNF
* Schreibe $$\theta \lor ( \phi \land \psi) $$ um zu $$(\theta \lor \phi) \land (\theta \lor \psi)$$
---
* Schreibe $$(\phi \land \psi) \lor \theta$$ um zu $$(\phi \lor \theta) \land (\psi \lor \theta)$$
---
* Schreibe $$(\phi \land \psi) \land \theta$$ um zu $$ \theta \land ( \phi \land \psi)$$
---
* Schreibe $$(\phi \lor \psi) \lor \theta$$ um zu $$ \theta \lor ( \phi \lor \psi)$$
---
</div>
<div class="nb-cell program" data-background="true" name="p3">
% cnf.pl
%nnf2cnf(X,Y,Z):- nl, write(X), write("...."), write(Y), write("...."), write(Z),fail.
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="q4">
nnf2cnf([[or(and(c,d), not(b))]],[],CNF).
</div>
<div class="nb-cell query" name="q5">
nnf2cnf([[or(and(a,b),and(c,or(d,e)))]],[],CNF).
</div>
<div class="nb-cell markdown" name="md4">
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="md5">
### CNF to setCNF
</div>
<div class="nb-cell program" data-background="true" name="p4">
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="q6">
setCnf([[not(b), not(a)]],SetCNF).
</div>
<div class="nb-cell query" name="q7">
trace, setCnf([[a,b,a,not(b)],[b,a,not(b)]],SetCNF).
</div>
<div class="nb-cell query" name="q8">
removeDuplicates([a,b,d,c,a,d,e,f],X).
</div>
<div class="nb-cell query" name="q9">
removeDuplicates([[a,b,c],[a,d,e],[c,b,a]],L).
</div>
<div class="nb-cell markdown" name="md6">
### Implementierung der Resolutionsregel:
</div>
<div class="nb-cell markdown" name="md7">
**main predicate**
</div>
<div class="nb-cell program" data-background="true" name="p6">
% propResolution.pl
rprove(Formula):-
cnf(not(Formula),CNF),
refute(CNF).
</div>
<div class="nb-cell markdown" name="md8">
**Steuerung des Resolutionsprozesses**
</div>
<div class="nb-cell program" data-background="true" name="p7">
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 markdown" name="md9">
**Resolutionsregel**
</div>
<div class="nb-cell program" data-background="true" name="p8">
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="q10">
resolve([p,s,not(t),r],[q,v,not(s),r],Result).
</div>
<div class="nb-cell markdown" name="md10">
### Examples Queries:
</div>
<div class="nb-cell query" name="q11">
write("Satz vom ausgeschlossenen Dritten: "), rprove(or(p,not(p))).
</div>
<div class="nb-cell query" name="q12">
write("Consequentia mirabilis: "), rprove(imp(imp(not(p),p),p)).
</div>
<div class="nb-cell query" name="q13">
write("Peircesches Gesetz: "), rprove(imp(imp(imp(p,q),p),p)).
</div>
<div class="nb-cell query" name="q14">
write("kein Theorem: "),rprove(or(not(p),q)).
</div>
<div class="nb-cell markdown" name="md11">
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>