Hi
Ich hätte mal eine allgemeine Frage zum Tableaukalkül mit PL1 (schon ein wenig her wo ich den gelernt hab):
Wenn ich in einem Ast die Prädikate
Code
P(a)
|
P(b)
|
Exists x ~P(x)Dann müsste ich für den Existenzquantor eine neue Skolem einführen - e.g. P(c) oder? D.h. Existenzquantor kann mir hier keinen Widerspruch liefern
Danke
LG
