<div class="notebook open-fullscreen">
<div class="nb-cell program" name="p11">
% Auszug aus foResolution.pl
%
% adapted by Wiebke Petersen
</div>
<div class="nb-cell program" data-background="true" name="p3">
% swish helper
:-style_check(-discontiguous).
:-style_check(-singleton).
</div>
<div class="nb-cell program" data-background="true" data-singleline="true" name="p2">
% 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 program" data-background="true" data-singleline="true" name="p10">
% printInfix/1: druckt eine in Präfix-Form gegebene Formel in Infix-Form.
printInfix(X):- numbervars(X,1,_End,[]),printInfix1(X).
printInfix1(X):- var(X), write(X),!.
printInfix1(not(X)):- write('~'), write('('), printInfix1(X), write(')'),!.
printInfix1(and(X,Y)):- write('('), printInfix1(X), write(' & '), printInfix1(Y), write(')'),!.
printInfix1(or(X,Y)):- write('('), printInfix1(X), write(' v '), printInfix1(Y), write(')'),!.
printInfix1(imp(X,Y)):- write('('), printInfix1(X), write(' > '), printInfix1(Y), write(')'),!.
printInfix1(eq(X,Y)):- write('('), printInfix1(X), write(' = '), printInfix1(Y), write(')'),!.
printInfix1(some(X, F)):- write('some ('), write_term(X,[numbervars(true)]), write(' '), printInfix1(F), write(')'),!.
printInfix1(all(X, F)):- write('all ('), write_term(X,[numbervars(true)]), write(' '), printInfix1(F), write(')'),!.
printInfix1(lam(X, F)):- write('lam '), write_term(X,[numbervars(true)]), write(' '), printInfix1(F),!.
printInfix1(app(X,Y)):- write('('), printInfix1(X), write(' @ '), printInfix1(Y), write(')'),!.
printInfix1(A):- write(A),!.
</div>
<div class="nb-cell markdown" name="md1">
## Implementing FOL Resolution
</div>
<div class="nb-cell markdown" name="md2">
FOL in CNF umwandeln:
</div>
<div class="nb-cell program" data-background="true" name="p1">
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="p4">
% 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="p5">
% 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 program" data-background="true" name="p6">
% nnf distinct from propositional logic
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).
% 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="md3">
### Resolution
</div>
<div class="nb-cell program" data-background="true" name="p7">
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="p8">
% 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="md4">
Abweichungen und Erweiterungen
</div>
<div class="nb-cell program" data-background="true" name="p9">
/*========================================================================
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="md5">
### Testanfragen:
</div>
<div class="nb-cell query" name="q1">
write("Theorem?"), rprove(all(X,or(p(X),not(p(X)))), Result).
</div>
<div class="nb-cell query" name="q2">
write("Theorem?"), rprove(imp(all(X,p(X)),not(some(Y,not(p(Y))))), Result).
</div>
<div class="nb-cell query" name="q3">
write("Theorem?"), rprove(some(X,or(p(X),q(X))), Result).
</div>
<div class="nb-cell query" name="q4">
write("Theorem?"), rprove(some(X,and(man(X),some(Y,woman(Y)))), Result).
</div>
<div class="nb-cell query" name="q5">
Formula=some(X,and(man(X),some(Y,woman(Y)))),
printInfix(Formula),
nl, % newline character
write("Theorem?"),
rprove(Formula,Result).
</div>
<div class="nb-cell markdown" name="md6">
Auch hier können wir die Formel in Infixnotation ausgeben:
</div>
</div>