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.
First order Tablau
Nur um sicherzugehn ob ich das richtig verstanden hab: exist quantoren kriegt man weg indem man subistituiert, wenn man dann eine resubsitution findet welche alle zweige schließt ist der tablau valid?
wie genau is des dann bei forall quantoren? heist das einfach das ich bei jedem zweig dann eine eigene substitution benutzen darf?
So verstehe ich das:
Für die Proposition “\forall X. A” kannst du theoretisch alle Propositionen “B/X” in deinen aktuellen Branch mit aufnehmen, wobei B ein Term ohne freie Variablen ist. Das sind natürlich unendlich viele, deshalb wirst du dir gezielt einige B’s aussuchen für die du das machen willst.
Für die Proposition “\exists X. \neg A” kannst du eine Proposition “c/X” in deinen aktuellen Branch mit aufnehmen, wobei c eine neue Skolemkonstante ist. Das ist im Prinzip das gleiche was bei der Umwandlung einer Formel in Klauselnormalform geschieht.
Sowohl Existenz- als auch Allquantoren öffnen keine neuen Branches sondern fügen einfach neue Formeln in ihren Branch ein.
Wenn du jetzt für “H \cup { \neg A }” ein geschlossenens Tableau findest, dann ist “H \cup { \neg A }” unerfüllbar und es gilt H ⊧ A.
1 „Gefällt mir“