Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Trinkerparadoxon - resolution
Ich habe irgendwo ein Denkfehler bei der Resolution (Blatt 12 Aufgabe 1)
∃x (P(x) → ∀y P(y))
= ∃x (-P(x) oder ∀y P(y))
Dann negieren: ∀x (P(x) und ∃y -P(y))
→ ∀x ∃y (P(x) und -P(y))
skolem: ∀x (P(x) und -P(f(x))
klauseln: {P(x)} {-P(f(x))}
und hier kommt ich nicht weiter, weil ich die beiden klauseln nicht substituieren kann.
Oder habe ich vergessen das zweite x umzubenennen, weil man prinzipiell gebundene Variablen immer umbenennen kann?
Danke im Voraus
Genau das 
Du musst sogar vor Anwendung von der Resolutionsregel (RIF) die Variablen umbenennen, sonst bekommst du ggf. einen kleineren MGU (siehe Skript bei Einführung von (RIF)).
Ich würde das auf Papier dann so hinschreiben:
{P(x)} {~P(f(x))} = {~P(f(x'))}
| |
----------------------- [f(x')/x]
|
v
{ }