7.5

[koe]

Mir war heute in der Vorlesung a bissal fad und da hab ich gleich einmal a paar Beispiele vom 7-er Zettel gemacht!
*g*
Das ist meine Lösung vom Beispiel 7.5!

lg
koe

[NightHaG]

hab ich genauso :)

[ChristofNeutron]

:confused: Ich steh da total an :confused:
Kann mir vielleicht irgendjemand der's verstanden hat erklären, wei man das liest??? Ich war zwar in der VO habs aber dort auch schon nicht kapiert :(
Ich weiß zwar, dass man die Bsp von unten nach oben aufbaut, aber wann ich da was wo (rechts oder links) hinschreib, und was ich da wann oder wo schon erledigt habe, bzw. noch beachten muss :shinner:
Also ich kapiers nicht :(

*edit* Also nach ein bisl stöbern im Forum (jaja, die Suchfunktion ist echt nicht schlecht ;) ) bin ich auf eine ziemllich gute Erklärung gestoßen.
http://hades.gothic.at/iforum/showthread.php?t=9514 speziell der 6 Beitrag hat sehr zum Verständniss beigetragen :thumb: :)

[jamironico]

kann mir jemand erklaeren wie man auf ein gegenmodell kommt und wann man weiss ob eine formel gueltig ist oder nicht. ich weiss wie man das ganze ableitet, aber ich was nicht was ich mit dem ganzen anfangen soll.

wie ichs verstanden habe, ist eine formel dann gueltig wenn axiome von der ableitung raus kommt. stimmt das? und wie komme ich dann auf ein gegenmodell falls kein axiom raus kommen sollte?

[ein_stein2000]

also i versteh das system mit dem ableiten überhaupt net .... i sitz jetzt seit 2 stunden vor dem skritpum und dem beispiel und finde ka system :(

gibts da ne erklärung von student zu student für mich? :D

[Erdbeere]

Wer kann diese Beispiel erklaeren?
Ich habe nichts verstanden...:traurig:
Wie funktioniert das?:hewa:

[owaye]

naja, ich probier mal ansatzmässig, und hoffe, die größten unklarheiten beseitigen zu können: :distur:

die formeln für das sequenzialkalkül sind im buch drin: es gibt genau 8 formeln. das umgekehrte T, ich schreibe es jetzt so " l- " ist ein relationszeichen. nehmen wir also ein beispiel:

(H ^ K),C,E

schritt_1: ich setze einfach das l- an den anfang des terms (das macht man halt einfach) =>

_______________
l- (H ^ K),C,E


gut, jetzt habe ich einen ausdruck rechts vom relationszeichen stehen.
wie gehts weiter? ich muss den term mit den komischen ausdrücken "nicht|impliziert|oder|und" wegkriegen. das geht eben mit den formeln im buch. welche nehme ich aber jetzt? =>
weil der ganze ausdruck RECHTS vom relationszeichen steht, kann ich nur eine von den vier -r (r steht für rechts) formeln nehmen. da ein ^ symbol eliminiert werden muss nehm ich also ^-r sieht dann so aus


_______________ ^-r
l- (H ^ K),C,E



die formel lautet im buch so:

F l- G,A F l- G,B
_________________________
F l- G,A^B


wir müssen STUR nach dieser formel gehen, also:
F ist einfach ein funktionsterm (zB. (A v B) oder nur die variablen durch beistrich getrennt)
G dasselbe

A ist der vordere ausdruck das mit dem "^" -zeichen zu tun hat
B der hintere ausdruck

*** in demfall entspricht A unserem H, und B unserem K.
*** das G in der formel entspricht unserem C,E
*** links vom ausdruck steht bei uns nichts (also weder ein ausdruck, noch irgendeine variable), also brauchen wir das "F" nicht.

Achtung!!! wenn da steht A^B kann es auch sein, dass A ein ausdruck wie
(D v G) ist, und B einer wie (Z v B). das ganze würde dann so aussehen:

(D v G)^(Z v B) wobei das jeweils unterstrichene dem
______ _______
A B entspricht. dasselbe gilt übrigens auch für G und F.



aber machen wir jetzt bei unserem beispiel weiter, also:

l- C,E,H l- C,E,K
______________________________ ^-r
l- (H ^ K),C,E

das wäre die lösung.
für obige zeile gilt:

wir haben darum nichts links vom relationszeichen stehen, weil auch der ausdruck darunter nichts links vom zeichen gehabt hat, also kein "F". rechts vom relationszeichen befindet sich "G", also unser C,E und dann das "A", also unser 'H' von H^K. da das ganze wird aufgespalten, wie man ja gesehen hat, nun zum ausdruck ganz rechts: für F haben wir ebenfalls nichts gehabt, deswegen beginnts gleich mit dem relationenzeichen l-, und dann steht das "G" (unser C,E) und dann das "B" (unser K).
voilà, das wars.
natürlich ist das im beispiel mehr verschachtelt, aber man muss prinzipiell nur STUR den formeln nachgehen, ziemlich pingelig das ganze und der kopf muss arbeiten.

so, ich hoff das hat a bissl was geholfen, wär leichter wenn das mündlich ging
schriftlich ist ur-mühsam.

ahja, noch einen tipp zum auflösen: wenn man einen ausdruck hat wie:
((A^B)v(C^D))vC beginn ich immer zuerst die klammer aufzulösen, die das ganze "umfasst".
wir würden hier für en ausdruck A das nehmen =>
((A^B)v(C^D))
und für den Ausdruck B das nehmen =>
C

und die operation die erfolgt, wäre hier ein v-r am anfang. in der darauffolgenden zeile dann müssten wir dann das "v" zwischen (A^B) und (C^D) auflösen...

:shinner:


würde dann so aussehen:
l- (A^B)v(C^D),C
____________________ v-r
l- ((A^B)v(C^D))vC


für G und F haben wir hier nichts. nachher siehts dann so aus:


l- C,(A^B),(C^D)
____________________ v-r
l- (A^B)v(C^D),C
____________________ v-r
l- ((A^B)v(C^D))vC


wie man sieht, entspräche in er zweiten zeile das C dem "berüchtigten" "G" in der sturen formel. nächste zeile so:

l- C,A,(C^D) l- C,B,(C^D)
____________________________________ ^-r
l- C,(A^B),(C^D)
____________________ v-r
l- (A^B)v(C^D),C
____________________ v-r
l- ((A^B)v(C^D))vC

jetzt wirds gschissen... wie man sieht: also. links hab ich darum stehen l- C,A,(C^D) weil
***ich nehme ja nur 1 term zum auflösen, diesmal also A^B, dass sich eben so aufspaltet: das A geht nach links, das B nach rechts, und G entspräche jetzt den restlichen funktionen rechts vom relationenzeichen, also das wären in demfall C und (C^D), angeschrieben als C,(C^D); wird einfach laut formel angehängt.

wenn es zu einer aufspaltung kommt, und man bekommt ein antiaxion raus, kann man sich den anderen zweig sparen und wegstreichen; ansonsten müssen beide zweige für sich gemacht werden.

naja, und dann gehts weiter (nein nein, das mach ich jetzt nicht mehr :shinner: oder eben man muss auf beiden extra weitermachen, wenn nichts weggeht)

so, das wars *schwitz*, hoff mal einen kleinen durchblick verschafft zu haben, mfg

[grassi3000]

Wie funkt das eigentlihc mit dem Gegenbeispiel. Das nehme ich beim b) um zusätzlich zu den Ableitungen zu zeigen, dass es nicht gültig ist`?

[nautiLus]

Cool erklärt, owaye...
Ich checks zwar noch nicht 100% aber die Erklärung ist sehr gut.
Ich glaub es wird dann ein Lichtlein aufgehen, wenn man sich mal zu einem Beispiel der Übung setzt und das durchkaut. Das werd ich jetzt mal machen..
thx
ciao, Nauti

edit: so aber jetzt hab ich alles gecheckt.... :) thx nochmal an owaye!
einzig noch das mit dem Gegenmodell versteh ich noch nicht ganz so wie grassi3000 und jamironico.
Kann das mal wer erklären wie man das macht usw.. :confused: cu

[stichri]

also wir stellen mal unsere lösungen vom montag online.
haben meistens die seitenzahl dazugeschrieben wo's im skriptum steht
hoffe ihr könnts lesen...

http://websrv.netparknet.at/oejab/chris/uni/theoinf/UE7/7_5_1.jpg
http://websrv.netparknet.at/oejab/chris/uni/theoinf/UE7/7_5_2.jpg


alle lösungen für UE7
http://websrv.netparknet.at/oejab/chris/uni/theoinf/UE7/

anna & chris

[Veronika]

kann mir jemand erklaeren wie man auf ein gegenmodell kommt und wann man weiss ob eine formel gueltig ist oder nicht. ich weiss wie man das ganze ableitet, aber ich was nicht was ich mit dem ganzen anfangen soll.

wie ichs verstanden habe, ist eine formel dann gueltig wenn axiome von der ableitung raus kommt. stimmt das? und wie komme ich dann auf ein gegenmodell falls kein axiom raus kommen sollte?
Also wahrscheinlich hast du eh schon längst eine Antwort, aber trotzdem:
Dass eine Formel dann gueltig ist, wenn axiome (und nur axiome) rauskommen, ist richtig. Gegenmodell am einfachsten:
das, was rechts vom |- steht, f setzen,

z.B. wenn rauskommt:

|- A,C was kein Axiom ist, dann setzt du A und C auf f

[Superwinki]

also wir stellen mal unsere lösungen vom montag online.
haben meistens die seitenzahl dazugeschrieben wo's im skriptum steht
hoffe ihr könnts lesen...

Ist zwar sehr nett aber ab der Linksableitung, wo es sich in zwei Pfade aufsplittet stimmt das nicht mehr.
Die Zeile direkt darüber müsste doch korrekterweise heißen:


A impl E |- B,C, A impl E A impl E, B ^ C |- B,C