Prädikatenlogische Resolution

Neue Frage »

Auf diesen Beitrag antworten »
Haevelin 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?
 
Auf diesen Beitrag antworten »
Haevelin RE: Prädikatenlogische Resolution

Wie kann ich das in Latex darstellen?
Auf diesen Beitrag antworten »
ed209

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 großes Grinsen ):
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
Auf diesen Beitrag antworten »
Haevelin

Die Formeln sind durch Skolemisierung auch ohne Axiomensystem und Individuenbereich lösbar.
 
Auf diesen Beitrag antworten »
ed209

Zitat:

Die Formeln sind durch Skolemisierung auch ohne Axiomensystem und Individuenbereich lösbar.

Nagut, wenn du das sagst. Aber nicht von mir Augenzwinkern
Auf diesen Beitrag antworten »
Haevelin 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?
 
Neue Frage »
Antworten »


Verwandte Themen

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