Prädikatenlogische Resolution |
11.04.2017, 08:29 | Haevelin | Auf diesen Beitrag antworten » |
Prädikatenlogische Resolution ((!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? |
||
12.04.2017, 16:25 | 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. |
|
Verwandte Themen
Die Beliebtesten » |
|
Die Größten » |
Die Neuesten » |
|