Not logged in. · Lost password · Register

Vvalter
Member since Dec 2012
119 posts
Subject: Free variable Tableaux
Ich glaube das Free variable Tableaux soweit zu verstehen, habe aber noch ein paar Probleme mit der genauen Definition.

In den notes wird erwähnt, dass die witness Skolemvariable bei der exists Regel von allen Metavariablen abhängen muss, aber in der Regeldefinition wird es von allen freien Variablen abhängig gemacht. Es kann doch auch freie Variablen geben, die keine Metavariablen sind oder?

In dem Beispiel 13.1.11 auf note 429 instanziieren wir y durch a. Danach steht auf der rechten Seite q(b)T und q(a)F. Rein nach Definition sollten wir jetzt hier doch auch die false Regel anwenden dürfen, weil wir ja z.b. [a/b] als MGU finden können.

Also im wesentlichen kommt es mir so vor als ob hier freie Variablen allgemein und Metavariablen durcheinander geworfen werden...
Jazzpirate
Member since Oct 2016
803 posts
In den notes wird erwähnt, dass die witness Skolemvariable bei der exists Regel von allen Metavariablen abhängen muss, aber in der Regeldefinition wird es von allen freien Variablen abhängig gemacht. Es kann doch auch freie Variablen geben, die keine Metavariablen sind oder?
...kann es theoretisch, wenn die Formel kein Satz ist (i.e. von vorneherein freie Variablen beinhält). In dem Fall "musst" du zumindest semantisch eh den universellen Abschluss der Formel betrachten, dann hast du a bunch of allquantoren, die du dann loswerden musst, indem du metavariablen einführst... ;-)
Also, tl;dr: oBdA sind alle freien variablen metavariablen :-)

weil wir ja z.b. [a/b] als MGU finden können.
b ist keine Variable; Konstanten darfst du nicht ersetzen ;-)
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