 Prädikatenlogische Resolution |
Haevelin
Tripel-As
Dabei seit: 04.06.2013
Beiträge: 221
 |
|
| 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?
|
|
10.04.2017 15:43 |
|
|
Haevelin
Tripel-As
Dabei seit: 04.06.2013
Beiträge: 221
|
|
| RE: Prädikatenlogische Resolution |
|
Wie kann ich das in Latex darstellen?
|
|
|
11.04.2017 15:58 |
|
|
ed209
Routinier
Dabei seit: 07.09.2006
Beiträge: 324
|
|
Hi Haevlin
Die Logik dahinter sieht ganz vernuenftig aus.
Aber hier mal was ganz Grundsaetzliches zu Logikfragen und eigentlich allem was mit theoretischer Informatik zu tun hat:
Jedes logische Kalkuel besteht aus bestimmten Axiomen und Schlussregeln. Wenn immer ein Professor eine Frage zu Logik stellt, bezieht er sich auf ein bestimmtes Axiomssystem (im Normalfall das was in der Vorlesung dran kam).
Ohne diesen Kontext ergeben die Fragen fuer die meisten die die Frage hier lesen keinen Sinn, oder wenn sie es tun nur zufaellig weil sie sich auf ein aehnliches System beziehen.
Das birgt aber eine Gefahr. Nur weil ich dir sage, dass deine Folgerung gut aussehen fuer mich und richtig sind heisst das nicht dass dein Korrektor es genau so sieht.
Eine Schlussregel die fuer mich gueltig und eindeutig ist, ist eventuell unvollstaendig fuer jemanden anderes.
Deswegen mein Hinweis an alle (am besten macht jemand daraus ein Sticky Post oder so 
):
Wenn immer Ihr eine Frage zu was theoretischem habt, sei es Logik, Komplexitaetstheorie, was grundlegendes mit Automaten oder was auch immer. Gebt immer alle Definitionen und Regeln mit an! Ohne die sind die Aufgaben nicht eindeutig loesbar.
Gruss,
ED
|
|
|
14.04.2017 16:18 |
|
|
Haevelin
Tripel-As
Dabei seit: 04.06.2013
Beiträge: 221
|
|
Die Formeln sind durch Skolemisierung auch ohne Axiomensystem und Individuenbereich lösbar.
|
|
|
20.04.2017 11:23 |
|
|
ed209
Routinier
Dabei seit: 07.09.2006
Beiträge: 324
|
|
| Zitat: |
Die Formeln sind durch Skolemisierung auch ohne Axiomensystem und Individuenbereich lösbar.
|
Nagut, wenn du das sagst. Aber nicht von mir 
|
|
|
23.04.2017 05:33 |
|
|
Haevelin
Tripel-As
Dabei seit: 04.06.2013
Beiträge: 221
|
|
| RE: Prädikatenlogische Resolution |
|
| Zitat: |
Original von Haevelin
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? |
Das Problem ist der Übergang zu Ex Ay Ey' Ax' (!P(x,y) et P(x',y'); daraus gewinnt man nicht: Ay Ax' (!P(c,y) et P(x', d))
die Frage ist, ob der Übergang früher möglich ist: also von:
(Ex Ay !P(x,y)) et (Ey'Ax'P(x',y'))
zu : Ay Ax' (!P(c,y) et P(x', d))
Das könnte man durch E Elimination erreichen. Aber bei der Gewinnung einer Klausalmenge könnte das unter Umständen problematisch sein. Darf man das?
|
|
|
24.04.2017 10:11 |
|
|
|
