---

Geschrieben von Haevelin am 10.04.2017 um 15:43:

  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?

---

Geschrieben von Haevelin am 11.04.2017 um 15:58:

  RE: Prädikatenlogische Resolution

Wie kann ich das in Latex darstellen?

---

Geschrieben von ed209 am 14.04.2017 um 16:18:

 

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

---

Geschrieben von Haevelin am 20.04.2017 um 11:23:

 

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

---

Geschrieben von ed209 am 23.04.2017 um 05:33:

 

Zitat:

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

Nagut, wenn du das sagst. Aber nicht von mir

---

Geschrieben von Haevelin am 24.04.2017 um 10:11:

  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?