08.02.00GK Prolog: Prolog und Prädikatenlogik II 1 Prolog und Prädikatenlogik II Prolog Grundkurs...

08.02.00 GK Prolog: Prolog und Prädikatenlogik II

1

Prolog und Prädikatenlogik IIProlog und Prädikatenlogik II

Prolog Grundkurs WS 99/00

Christof Rumpf

[email protected]


2

translate/1translate/1

translate(X):- implout(X,X1),nl, negin(X1,X2), skolem(X2,X3,[]), univout(X3,X4), cnf(X4,X5), clausify(X5,Clauses,[]),

prologify2(Clauses,Clauses2), pclauses(Clauses2).

Implikationen umformen

Negationen einwärts

Skolemisierung

Allquantoren eliminieren

Konjunktive Normalform

Klauselform

Hornklauseln

Prolog-Klauseln


3

implout/2implout/2 - I - I

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).


4

implout/2implout/2 - II - II

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).


5

negin/2negin/2 & & neg/2neg/2

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)).


6

skolem/3skolem/3

skolem(all(X,P), all(X,P1), Vars):- !, skolem(P, P1, [X|Vars]). skolem(exists(X,P), P2, Vars):- !, gensym(c,F), Sk =.. [F|Vars], subst(X, Sk, P, P1), skolem(P1, P2, Vars). skolem((P + Q), (P1 + Q1), Vars):- !, skolem(P, P1, Vars), skolem(Q, Q1, Vars). skolem((P # Q), (P1 # Q1), Vars):- !, skolem(P, P1, Vars), skolem(Q, Q1, Vars). skolem(P,P,_).


7

gensym/2gensym/2

gensym(Root,Symbol):- name(Root,L1), symb(Root,S), name(S,L2), conc(L1,L2,L3), name(Symbol,L3).

symb(R,S1):- retract(gensymsym(R,S)), !, inc(S,S1), assert(gensymsym(R,S1)).

symb(R,0):- init_gensym(R).

init_gensym(R):- retract(gensymsym(R,_)), fail. init_gensym(R):- assert(gensymsym(R,0)), !.


8

subst/4subst/4

subst(X,S,T,S):- X == T, !. subst(_,_,T,T):- var(T) ; atomic(T), !. subst(X,S,P,P1):- P =.. L, substl(X,S,L,L1), P1 =.. L1.

substl(_,_,[],[]):- !. substl(X,S,[H1|T1],[H2|T2]):- subst(X,S,H1,H2), substl(X,S,T1,T2).


9

univout/2univout/2

univout(all(X,P), P1):- !, univout(P,P1).

univout((P + Q), (P1 + Q1)):- !, univout(P, P1), univout(Q, Q1). univout((P # Q), (P1 # Q1)):- !, univout(P, P1), univout(Q, Q1). univout(P, P).


10

cnf/2cnf/2

cnf((P # Q), R):- !, cnf(P, P1), cnf(Q, Q1), cnf1((P1 # Q1), R). cnf((P + Q), (P1 + Q1)):- !, cnf(P, P1), cnf(Q, Q1). cnf(P, P).


11

cnf1/2cnf1/2

cnf1(((P + Q) # R), (P1 + Q1)):- !, cnf((P # R), P1), cnf((Q # R), Q1). cnf1((R # (P + Q)), (P1 + Q1)):- !, cnf((R # P), P1), cnf((R # Q), Q1). cnf1(P, P).


12

clausify/3clausify/3

clausify((P + Q), C1, C2):- !, clausify(P, C1, C3), clausify(Q, C3, C2). clausify(P, [cl(A, B)|Cs], Cs):- inclause(P, A, [], B, []), !. clausify(_, C, C).


13

inclause/5inclause/5

inclause((P # Q), A, A1, B, B1):- !, inclause(P, A2, A1, B2, B1), inclause(Q, A, A2, B, B2). inclause((^P), A, A, B1, B):- !, notin(P, A), putin(P, B, B1). inclause(P, A1, A, B, B):- !, notin(P, B), putin(P, A, A1).


15

pclauses/1pclauses/1 & & pclause/2pclause/2

pclauses([]):- !, nl. pclauses([cl(A,B)|Cs]):- pclause(A, B), nl, tab(4), pclauses(Cs).

pclause(L, []):- !, pdisj(L), write('.'). pclause([], L):- !, write(':- '), pconj(L), write('.'). pclause(L1,L2):- pdisj(L1), write(':- '), pconj(L2), write('.').


16

pdisj/1pdisj/1 & & pconj/1pconj/1

pdisj([L]):- !, write(L). pdisj([H|T]):- write(H), write('; '), pdisj(T).

pconj([L]):- !, write(L). pconj([H|T]):- write(H), write(', '), pconj(T).


17

prologify1/2prologify1/2 % Solution 1: produces infinite loops with indirect recursions. % Clauses with n disjuncts in the head are transformed to n

clauses % with single heads. Every disjunct gets its own clause where it % represents the single head of the clause while all other

disjuncts % become negated conjuncts in the body of that clause.

prologify1([],[]):- !. prologify1([cl(H,B)|Cs],Clauses):- prologify_clause1(H,H,B,Clauses1), prologify1(Cs,Clauses2), append(Clauses1,Clauses2,Clauses).


18

prologify_clause1/2prologify_clause1/2

prologify_clause1([],_,_,[]):- !. prologify_clause1([H|T],Disj,B,[cl([H],B2)|Cs]):- delete(H,Disj,NegConj), !, prologify_disj1(NegConj,B1), append(B,B1,B2), prologify_clause1(T,Disj,B,Cs).

prologify_disj1([],[]):- !. prologify_disj1([D|Ds],[not(D)|Cs]):- prologify_disj1(Ds,Cs).


19

prologify2/2prologify2/2 % Solution 2: selects the first disjunct as the head of the clause. % The first disjunct in the complex head of a clause is arbitrarily % choosen to represent the single head of the clause, while all

other % disjuncts become negated conjuncts in the body of that clause.

prologify2([],[]):- !. prologify2([cl(H,B)|Cs],[Clause|Clauses]):- prologify_clause2(H,H,B,Clause), prologify2(Cs,Clauses). prologify_clause2([],_,_,[]):- !. prologify_clause2([H|T],Disj,B,cl([H],B2)):- delete(H,Disj,NegConj), !, prologify_disj(NegConj,B1), % as for the 1st solution append(B,B1,B2).


20

prologify3/2prologify3/2

% Solution 3: perform an intelligent search on the clauses to find out % which predicates are already defined or have to be defined to % allow decuctions from the database. Facts might give rise to

the % decision that their predicated should not appear as rule heads % unless the rule includes recusion on that predicate.

% ...to be implemented...


21

Alle Menschen sind sterblich.Alle Menschen sind sterblich.

PL1 all(A,mensch(A) -> sterblich(A))

IMP all(A,^ mensch(A) # sterblich(A))

NEG all(A,^ mensch(A) # sterblich(A))

SKO all(A,^ mensch(A) # sterblich(A))

UNI ^ mensch(A) # sterblich(A)

CNF ^ mensch(A) # sterblich(A)

CL1 [cl([sterblich(A)],[mensch(A)])]

CL2 [cl([sterblich(A)],[mensch(A)])]

PRO sterblich(A):- mensch(A).


22

Alle Männer lieben irgendeine Frau.Alle Männer lieben irgendeine Frau.

PL1 all(A,man(A) -> exists(B,woman(B) + loves(A,B)))

IMP all(A,^ man(A) # exists(B,woman(B) + loves(A,B)))

NEG all(A,^ man(A) # exists(B,woman(B) + loves(A,B)))

SKO all(A,^ man(A) # woman(c4(A)) + loves(A,c4(A)))

UNI ^ man(A) # woman(c4(A)) + loves(A,c4(A))

CNF (^ man(A) # woman(c4(A))) + ^ man(A) # loves(A,c4(A))

CL1 [cl([woman(c4(A))],[man(A)]),cl([loves(A,c4(A))],[man(A)])]

CL2 [cl([woman(c4(A))],[man(A)]),cl([loves(A,c4(A))],[man(A)])]

PRO woman(c4(A)):- man(A).

loves(A,c4(A)):- man(A).


23

Irgendein Mann liebt irgendeine Frau.Irgendein Mann liebt irgendeine Frau.

PL1 exists(A,man(A) + exists(B,woman(B) + loves(A,B))) IMP exists(A,man(A) + exists(B,woman(B) + loves(A,B))) NEG exists(A,man(A) + exists(B,woman(B) + loves(A,B))) SKO man(c2) + woman(c3) + loves(c2,c3) UNI man(c2) + woman(c3) + loves(c2,c3) CNF man(c2) + woman(c3) + loves(c2,c3) CL1 [cl([man(c2)],[]),cl([woman(c3)],[]),cl([loves(c2,c3)],[])] CL2 [cl([man(c2)],[]),cl([woman(c3)],[]),cl([loves(c2,c3)],[])] PRO man(c2). woman(c3). loves(c2,c3).


24

vorfahr/2vorfahr/2

NLS Elternteile von Individuen sind Vorfahren dieser Individuen und

Elternteile von Vorfahren von Individuen sind Vorfahren dieser Individuen.

PL1 all(A,all(B,all(C,(et(A,C) + v(C,B) -> v(A,B)) + (et(A,B) -> v(A,B)))))

IMP all(A,all(B,all(C,(^ (et(A,C) + v(C,B)) # v(A,B)) + ^ et(A,B) # v(A,B))))

NEG all(A,all(B,all(C,((^ et(A,C) # ^ v(C,B)) # v(A,B)) + ^ et(A,B) # v(A,B))))

SKO all(A,all(B,all(C,((^ et(A,C) # ^ v(C,B)) # v(A,B)) + ^ et(A,B) # v(A,B))))

UNI ((^ et(A,B) # ^ v(B,C)) # v(A,C)) + ^ et(A,C) # v(A,C)

CNF ((^ et(A,B) # ^ v(B,C)) # v(A,C)) + ^ et(A,C) # v(A,C)

CL1 [cl([v(A,C)],[et(A,B),v(B,C)]),cl([v(A,C)],[et(A,C)])]

CL2 [cl([v(A,C)],[et(A,B),v(B,C)]),cl([v(A,C)],[et(A,C)])]

PRO v(A,C):- et(A,B), v(B,C).

v(A,C):- et(A,C).

08.02.00GK Prolog: Prolog und Prädikatenlogik II 1 Prolog und Prädikatenlogik II Prolog Grundkurs...

Documents

Transcript of 08.02.00GK Prolog: Prolog und Prädikatenlogik II 1 Prolog und Prädikatenlogik II Prolog Grundkurs...