Treba da u Prologu napisem program koji standardnu logicku formulu prebacuje u preneks formu.
Za sada sam definisao operatore
Code:
?- op(200, fx, ~).
?- op(400, xfy, #).
?- op(400, xfy, &).
?- op(700, xfy, ->).
?- op(700, xfy, <->).
?- op(200, fx, ~).
?- op(400, xfy, #).
?- op(400, xfy, &).
?- op(700, xfy, ->).
?- op(700, xfy, <->).
izbacio implikaciju i ekvivalenciju
Code:
implout((P <-> Q), ((P1 & Q1) # (~P1 & ~Q1))) :- !, implout(P, P1), implout(Q, Q1).
implout((P -> Q), (~P1 # Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout(all(X, P), all(X, P1)) :- !, implout(P, P1).
implout(exists(X, P), exists(X, P1)) :- !, implout(P, P1).
implout((P & Q), (P1 & Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout((P # Q), (P1 # Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout((~P), (~P1)) :- !, implout(P, P1).
implout(P, P).
implout((P <-> Q), ((P1 & Q1) # (~P1 & ~Q1))) :- !, implout(P, P1), implout(Q, Q1).
implout((P -> Q), (~P1 # Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout(all(X, P), all(X, P1)) :- !, implout(P, P1).
implout(exists(X, P), exists(X, P1)) :- !, implout(P, P1).
implout((P & Q), (P1 & Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout((P # Q), (P1 # Q1)) :- !, implout(P, P1), implout(Q, Q1).
implout((~P), (~P1)) :- !, implout(P, P1).
implout(P, P).
i pomerio negaciju do atomske formule
Code:
negin((~P), P1) :- !, neg(P, P1).
negin(all(X, P), all(X, P1)) :- !, negin(P, P1).
negin(exists(X, P), exists(X, P1)) :- !, negin(P, P1).
negin((P & Q), (P1 & Q1)) :- !, negin(P, P1), negin(Q, Q1).
negin((P # Q), (P1 # Q1)) :- !, negin(P, P1), negin(Q, Q1).
negin(P, P).
neg((~P), P1) :- !, negin(P, P1).
neg(all(X, P), exists(X, P1)) :- !, neg(P, P1).
neg(exists(X, P), all(X, P1)) :- !, neg(P, P1).
neg((P & Q), (P1 # Q1)) :- !, neg(P, P1), neg(Q, Q1).
neg((P # Q), (P1 & Q1)) :- !, neg(P, P1), neg(Q, Q1).
neg(P, (~P)).
negin((~P), P1) :- !, neg(P, P1).
negin(all(X, P), all(X, P1)) :- !, negin(P, P1).
negin(exists(X, P), exists(X, P1)) :- !, negin(P, P1).
negin((P & Q), (P1 & Q1)) :- !, negin(P, P1), negin(Q, Q1).
negin((P # Q), (P1 # Q1)) :- !, negin(P, P1), negin(Q, Q1).
negin(P, P).
neg((~P), P1) :- !, negin(P, P1).
neg(all(X, P), exists(X, P1)) :- !, neg(P, P1).
neg(exists(X, P), all(X, P1)) :- !, neg(P, P1).
neg((P & Q), (P1 # Q1)) :- !, neg(P, P1), neg(Q, Q1).
neg((P # Q), (P1 & Q1)) :- !, neg(P, P1), neg(Q, Q1).
neg(P, (~P)).
Posle toga ostaje da se (1) preimenuju vezana pojavljivanja promenljivih, i (2) da se kvantori pomere ispred formule.
Sa (2) bih se i izborio, ali (1) mi zadaje velike probleme. Svaka pomoc je dobrodosla.
Hvala unapred!