Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
:- op(200,fx,'atm'). :- op(300,fx,'neg'). :- op(400,yfx,'und'). :- op(500,yfx,'oder'). :- op(600,xfx,'imp'). % nnf(+Formel,-NNFFormel) nnf(F1 und F2, R) :- !,nnf(F1,R1),nnf(F2,R2),R=R1 und R2. nnf(F1 oder F2, R) :- !,nnf(F1,R1),nnf(F2,R2),R=R1 oder R2. nnf(F1 imp F2, R) :- !,nnf((neg F1) oder F2, R). nnf(neg(F1 und F2), R) :- !,nnf(neg F1,R1), nnf(neg F2, R2), R=R1 oder R2. nnf(neg(F1 oder F2), R) :- !,nnf(neg F1,R1), nnf(neg F2, R2), R=R1 und R2. nnf(neg(F1 imp F2), R) :- !,nnf(F1,R1), nnf(neg F2, R2), R=R1 und R2. nnf(neg(neg(F)), R) :- !,nnf(F,R). nnf(neg(atm L), neg(atm L)) :-!. nnf(atm L, atm L). % Wandelt eine Formel in KNF um % knf(+Formel,-ResFormel). knf(A, D) :- remove_imp(A, B), deMorgan(B, C), toKNF_loop(C, D). % entferne imp remove_imp(neg F1, R) :-!, remove_imp(F1, R1), R = neg R1. remove_imp(F1 und F2, R) :-!, remove_imp(F1, R1), remove_imp(F2, R2), R = R1 und R2. remove_imp(F1 oder F2, R) :-!, remove_imp(F1, R1), remove_imp(F2, R2), R = R1 oder R2. remove_imp(F1 imp F2, R) :-!, remove_imp(F1, R1), remove_imp(F2, R2), R = neg R1 oder R2. remove_imp(A, A). % ziehe Negationen nach innen (de'Morgan) deMorgan(neg (neg F1), R) :-!, deMorgan(F1, R1), R=R1. deMorgan(neg (F1 und F2), R) :-!, deMorgan(neg F1, R1), deMorgan(neg F2, R2), R=R1 oder R2. deMorgan(neg (F1 oder F2), R) :-!, deMorgan(neg F1, R1), deMorgan(neg F2, R2), R=R1 und R2. deMorgan(F1 und F2,R) :-!, deMorgan(F1, R1), deMorgan(F2, R2), R=R1 und R2. deMorgan(F1 oder F2,R) :-!, deMorgan(F1, R1), deMorgan(F2, R2), R=R1 oder R2. deMorgan(A, A). toKNF(A oder (B und C), (A oder B) und (A oder C)) :-!. toKNF((A und B) oder C, (A oder C) und (B oder C)) :-!. toKNF(F1 und B, (R1 und B)) :-toKNF(F1, R1). toKNF(A und F2, (A und R2)) :-toKNF(F2, R2). toKNF(F1 oder B, (R1 oder B)) :-toKNF(F1, R1). toKNF(A oder F2, (A oder R2)) :-toKNF(F2, R2). toKNF_loop(A, C):-toKNF(A, B), ! ,toKNF_loop(B, C). toKNF_loop(A, A).