Not logged in. · Lost password · Register

Matombo
Member since Aug 2014
30 posts
Subject: 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?
frececroka
Member since Oct 2014
57 posts
+1 Jazzpirate
So verstehe ich das:

Für die Proposition "\forall X. A" kannst du theoretisch alle Propositionen "[B/X](A)" 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](A)" 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.
This post was edited on 2017-02-12, 14:52 by frececroka.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen