Prädikatenlogische Resolution

Neue Frage »

Haevelin Auf diesen Beitrag antworten »
Prädikatenlogische Resolution
Folgende Formel: wobei E ist Es gibt ein, und A = Für alle und != non

((!AxEy P(x,y)) et (Ey Ax P(x,y))
führt auf (!AxEy P(x,y)) et (Ey'Ax'P(x',y')
führt auf: (Ex Ay !P(x,y)) et (Ey'Ax'P(x',y')
führt auf: Ex Ay Ey' Ax' (!P(x,y) et P(x',y')
führt auf: Ay Ax' (!P(c,y) et P(x', d))
führt auf den Widerspruch !P(c,d) et P(c,d)

Ist das richtig?
Haevelin Auf diesen Beitrag antworten »
RE: Prädikatenlogische Resolution
Anders sieht es aus, wenn ich wie folgt vorgehe:
!AxEy P(x,y) et Ey Ax P(x,y)
daraus folgt: !Ax Ey Ey' Ax' (P(x,y) et P(x',y'))
daraus folgt: Ex Ay Ay' Ex' !( P(x,y) et P(x',y'))
daraus folgt: Ay Ay' !(P(c,y) et P(f(y,y'),y))
Daraus kann ich keine Resolution mehr durchführen. Diese Formel dürfte prinzipiell erfüllbar sein.
Neue Frage »
Antworten »



Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »