hi,
ich hab irgendwie ein komplettes verständnisproblem mit der herbrand-theorie. ich kann überhaupt nicht nachvollziehen, dass eine formel f erfüllbar ist, wenn es für f ein herbrand-modell gibt. denn wenn ich mir die beispielaufgabe (11.9) im skript ansehe, hab ich den eindruck, dass man die interpretation eines prädikatensymbols völlig willkürlich definieren kann (da die interpretation nicht restingiert ist). aber wenn das völlig willkürlich ist, kann ich mir die herbrand-strukturen doch immer so definieren, dass es mal ein modell gibt und mal nicht (wie in der beispielaufgabe). wo soll denn da die verbindung sein zwischen den willkürlichen herbrand-strukturen und der formel f?
komm da irgendwie gar nicht weiter… [img]http://www.fb18.de/gfx/wand.gif[/img]

der Punkt ist, dass du bei Herbrandmodellen nur festlegen darfst:
Domäne sowie Interpret. von P, f und c (jeweils Plural).
Du darfst z.B. nicht die Junktoren verändern, denn die
wurden ja schon (vgl. generelles Schema - ca. 100 mal im
Logik-Skript) durch das log. System L_{PL} definiert.
Die Formel A und nA kann daher auch in keinem Herbrandmod.
erfüllbar sein.
Für die H-M. wichtig zu verstehen ist meiner Meinung nach,
dass ein Term (z.B.) f© durch die Interpretation
auf die Zeichenkette "f©" abgebildet wird, dass es
auf der linken und rechten Seite der Zuweisung durch Interpr.
überhaupt nicht das selbe ist.

hm, also das mit den junktoren ist klar. also ist dann jede atomare formel (genau wie ein aussagensymbol) kontingent!?…


du meinst, dass rechts und links nicht dasselbe steht bei einer herbrand-interpretation, aber im skript steht, dass jeder geschlossene term aus der domäne durch sich selbst interpretiert wird: A(t) = t
oder ist da doch ein unterschied?

syntaktisch steht rechts und links in diesem Sinne das gleiche.
Allerdings ist die Bedeutung der Zeichen sehr unterschiedlich.
Von t^{I,A} = t (zur Unterscheidung t1^{I,A} = t2)
ist t1 ein Term, also eine Konstante, eine Variable oder ein Funktionssymbol mit
passenden Parametern (also auch Termen).
t2 hingegen ist die Zeichenkette "t". Nochmal anders:

[img]http://mokrates.de/cgi-bin/texstring?t1%20%5Cin%20Ter(L_%7BPL%7D)%20%5Cqquad%20%20t2%20%5Cin%20D[/img]

Christoph, wirf nicht so mit LOS-Sprache im Grundstudium rum ;)

also ist dann jede atomare formel (genau wie ein aussagensymbol) kontingent!?..

das dürfte doch klar sein..

Christoph, wirf nicht so mit LOS-Sprache im Grundstudium rum ;)

Huch! Ist ja F-Zyklus hier [img]http://www.fb18.de/gfx/16.gif[/img].
Aber naja, die Aussagen gelten trotzdem und der
Unterschied zwischen beiden Seiten kommt auch im
Grundstudium schon vor. Also wenn einer die Notation
nicht versteht… ignorieren oder nachfragen :)

hm, also das mit der interpretation ist mir noch etwas schleierhaft, aber ich setze mal voraus, dass das in der f-klausur nicht so wichtig sein wird.
aber danke für die hilfe, denn die herbrand-theorie ist mir um einiges klarer geworden

ich steh auch auf dem Schlauch, was Herby angeht. Und die LOS-Sprache ist mir nicht wirklich geläufig, bin auch zu faul zum Nachfragen.
Mir fehlt immernoch der Zugang zum Herbrand-Theorem. Was er machen soll ist klar. Erfüllbarkeit testen.

Nur das Wie ist mir schleierhaft. Was macht man denn nun? Im Skript blicke ich da noch nicht durch, und Übungsaufgaben habe ich noch leider keine gefunden zu Herbrand, die mir das ganze mal vorspielen würden.

Wenn sich einer erbarmen würde und sein Wissen mal auf die Probe stellen will, der darf das noch mal ruhig lang und breit, darstellen, was man da nun macht. Wäre cool, denn Herby ist das einzige was mir noch kopfschmerzen bereitet. der rest ist easy.

hier mal eine frühere Übungsaufgabe:
F1 = Vx Vy[ P(x,h(y,c)) -> -P(c,x)]
F2 = Vx [ Q(f(x)) v -Q(x)]
F3 = Q(h(a,f©))

Geben Sie für die Formeln F1,F2 und F3 jeweils ein Herbrand-Modell an und zeigen Sie, dass es tatsächlich ein Modell der jeweiligen Formel ist.

Also ich versuche mal, einen ganz groben Überblick zu geben,
mit dem du dann selbst versuchen kannst, die Theorie genau
zu verstehen.

Mir fehlt immernoch der Zugang zum Herbrand-Theorem. Was er machen soll ist klar. Erfüllbarkeit testen.
Nur das Wie ist mir schleierhaft.

(Ich nehme mal an, du meinst Satz 11.11.)
Das "Wie" steht auch im Satz noch nicht explizit drin. Der Satz
sagt zunächst nur, dass man für die Unerfüllbarkeit einer Formel
in Skolemform nur eine unerfüllbare Teilmenge der Herbrandexpansion
finden muss (und das macht man dann mit prädikatenlogischer
Resolution).

Das ist allerdings nicht das einzige, was man aus der Herbrand-
Theorie lernen kann. Z.B. sagt ja der Satz von Löwenheim-Skolem,
dass jede prädikatenlogische Formel ein abzählbares Modell besitzt
(und daran sieht man, dass man z.B. die reellen Zahlen nicht mit
solcher Prädikatenlogik definieren kann).

Als grober Überblick:
Allgemein erklärt die Herbrand-Theorie, auf welche Art von Modellen
man sich bei der Suche nach solchen beschränken kann (wenn man
nur wissen will, ob es welche gibt). Bei der Aussagenlogik
bereitete das noch keine Probleme: ein Modell war immer eine
von 2^n Belegungen, die man alle durchprobieren konnte.
In der Prädikatenlogik ist es aber nicht ganz so einfach: da ist
zunächst nicht klar, wie man systematisch auf die Suche nach
Modellen geht. In der Herbrand-Theorie erfährt man dann,
dass man sich nur für Herbrand-Strukturen interessieren muss.
Und im Spezialfall der Skolemform bedeutet das, dass man nur
noch prüfen muss, ob die Herbrand-Expansion aussagenlogisch
erfüllbar ist.

Was macht man denn nun?

Wenn man den Satz von Herbrand als Grundlage für ein
Verfahren verwenden will, um Unerfüllbarkeit zu untersuchen,
kann man prädikatenlogische Resolution machen (deren
Grundlage ist ja die Herbrand-Theorie). Dazu gab es doch
bestimmt Übungsaufgaben, oder?

Am besten du siehst dir die einzelnen Sätze im Skript an und
fragst dann, an welcher Stelle du was nicht verstehst.