Results 1 to 59 of 59

Thread: Übung Proof Theory

  1. #1
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts

    Übung Proof Theory

    Hab mir mal die proof theory Übung vorgenommen.

    ich komm auf:
    1. contradiction
    2. satisfiable
    3. valid
    4. valid
    5. satisfiable
    6. satisfiable

    wobei ich das 1. mit SC gezeigt hab. für ND bin ich mir nicht ganz sicher wie man da am besten vorgehen soll. wenn man die gesamte formel negiert, bekommt man ja not(A) und daraus lässt sich nur bottom ableiten. von bottom ausgehend kann man zwar ein beliebiges A, not(A) ableiten, aber das ist ja dann reines rumgerate...

    zu den interpretation:
    es sollte ja kein problem sein, satisfiable/falsifiable mit hilfe von dummy-prädikaten wie isInteger und integer als domain zu zeigen oder?

  2. #2
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Zur Interpretation: Da bin ich auch deiner Meinung.

    Was die Natural Deduction betrifft, muss ich gestehen, dass ich aus den Vorlesungsfolien noch nicht ganz schlau geworden bin. In diese Materie muss ich mich erst einlesen.

  3. #3
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Mir ist noch etwas eingefallen: "Negation Allquantor" entspricht ja "Existenzquantor Negation". Vielleicht hilft dir diese Regel beim Natural-Deduction-Beispiel.

  4. #4
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    versteh ich das richtig, dass du folgendes meinst:
    This image was created with the kind support of Paulchen
    darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...

  5. #5
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by _m@rt!n View Post
    versteh ich das richtig, dass du folgendes meinst:
    This image was created with the kind support of Paulchen
    Ja, genau das meinte ich.

    Quote Originally Posted by _m@rt!n View Post
    darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...
    Das weiß ich nicht. Wie gesagt, habe ich mich mit Natural Deduction noch nicht ausreichend auseinandergesetzt.

    Schreibst du die Hausübung mit LaTeX? Wie formatierst du die Beweise?

  6. #6
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Quote Originally Posted by _m@rt!n View Post
    darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...
    Hab mit den Beispielen zwar noch nicht begonnen, aber ich glaube dass solche Umformungen nicht erlaubt sind.

    Man befindet sich bei diesen Proofverfahren ja rein auf der syntaktischen Seite, sprich man darf wirklich nur "pattern-match-mäßig" die Regeln des jeweiligen Kalküls für einen Proof verwenden, aber kein "externes Wissen" über die Semantik der jeweiligen Logik.

  7. #7
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts

  8. The Following User Says Thank You to _m@rt!n For This Useful Post:


  9. #8
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by _m@rt!n View Post
    Hab mir mal die proof theory Übung vorgenommen.

    ich komm auf:
    1. contradiction
    2. satisfiable
    3. valid
    4. valid
    5. satisfiable
    6. satisfiable
    Wie lauten deine Gegenbeispiele bei 3 und 5?

    Ich tue mir beim Beweisen von 4 schwer - die Regel für den Existenzquantor links führt bei mir zu einer Aussage P(y) |- P(t), womit ich nichts anfangen kann.

  10. #9
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    3: is bei mir valid
    5: nimm zB isOdd und integers: es gibt nen integer der ungerade is, aber nicht alle integer sind ungerade: 1 -> 0

    4: immer zuerst die quantoren auflösen, die eine eugenvariable-condition haben, dann sollte es klappen
    Last edited by _m@rt!n; 03-04-2012 at 22:41. Reason: natürlich die mit eugenvariable nicht die ohne

  11. #10
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by _m@rt!n View Post
    5: nimm zB isOdd und integers: es gibt nen integer der ungerade is, aber nicht alle integer sind ungerade: 1 -> 0
    Das ist meines Erachtens kein Gegenbeispiel, denn wenn nicht alle Integer ungerade sind, gibt es einen Integer, der gerade ist, so dass die Implikation stimmt (0 -> 0). Ich glaube, die Formel 5 ist gültig.

  12. #11
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    hast recht, ich war da etwas vorschnell mit dem countermodel. das 5er is tatsächlich valid, man muss nur beim proven etwas herumprobieren. (Tipp: exists verdoppeln, weakening)

    hab dazu mal alle formeln durch nen prover geschickt, folgendes müsste demnach stimmen:
    1. contradiction
    2. satisfiable
    3. valid
    4. valid
    5. valid
    6. satisfiable
    Last edited by _m@rt!n; 04-04-2012 at 11:06.

  13. #12
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    um nochmal auf ND zurückzukommen, ist folgendes erlaubt?

    • canceln auf unterschiedlichen branches (also ich bekomme das [A] auf einem branch, möchte es aber auf einem anderen verwenden)
    • mehrfaches canceln (ich bekomme [A] und möchte damit 2mal A canceln)

  14. #13
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by _m@rt!n View Post
    hab dazu mal alle formeln durch nen prover geschickt, folgendes müsste demnach stimmen:
    Welchen Prover verwendest du? Gibt es ihn auch für DOS bzw. Windows?

  15. #14
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    ich verwende prover9-mace4. in den output von dem ding hab ich mich aber ehrlich gesagt nicht eingelesen. ich verwend es nur, um die ergebnisse zu verifizieren.

  16. The Following 2 Users Say Thank You to _m@rt!n For This Useful Post:


  17. #15
    Principal
    Join Date
    Oct 2006
    Location
    Wien/Salzburg
    Posts
    74
    Thanks
    8
    Thanked 10 Times in 6 Posts
    Quote Originally Posted by _m@rt!n View Post

    • canceln auf unterschiedlichen branches (also ich bekomme das [A] auf einem branch, möchte es aber auf einem anderen verwenden)
    Würde sagen das ist nicht erlaubt. Die Hypothese hat mit dem 'anderen' Branch nichts zutun.

    Quote Originally Posted by _m@rt!n View Post
    • mehrfaches canceln (ich bekomme [A] und möchte damit 2mal A canceln)
    Würd sagen ja. Auf dem Branch wo du [A] bekommen hast kannst du es immer zum Schließen des Zweiges verwenden.

    Angaben ohne Gewähr

  18. #16
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    das entspricht leider genau dem was ich vermutet hatte und vernichtet damit meinen proof :-(

    hat schon wer den ND-proof fürs erste beispiel geschafft?

  19. #17
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by _m@rt!n View Post
    hat schon wer den ND-proof fürs erste beispiel geschafft?
    Ich denk schon:
    man nimmt an, dass die Formel 1 wahr ist.
    R(b,b) -> -R(b,b).
    Annahme: R(b,b).
    -R(b,b).
    falsum.
    -R(b,b)
    Annahme: Formel 1 ist wahr.
    -R(b,b)->R(b,b)
    R(b,b)
    falsum
    nicht Formel 1

  20. #18
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    deine beschreibung hat mich zwar irgendwie verwirrt, aber zumindest so weit zum denken angeregt, dass ich ne lösung finden konnte (ich hab allerdings falsumx3 und eine RAA)

    eine letzte frage hab ich noch:
    wie formal habt ihr das mit der interpretation bei satisfiable/not valid gemacht?

    bei mir schaut das in etwa so aus:
    Domain=irgendwas
    This image was created with the kind support of Paulchen

    und dann noch ein paar sätze warum es unter dieser interpretation (k)ein model ist.

    möglicherweise ist das zu informell, aber andererseits denk ich mir, dass eine strikt formale interpretation irgendwie übertrieben ist.

  21. #19
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by _m@rt!n View Post
    eine letzte frage hab ich noch:
    wie formal habt ihr das mit der interpretation bei satisfiable/not valid gemacht?

    bei mir schaut das in etwa so aus:
    Domain=irgendwas
    This image was created with the kind support of Paulchen

    und dann noch ein paar sätze warum es unter dieser interpretation (k)ein model ist.

    möglicherweise ist das zu informell, aber andererseits denk ich mir, dass eine strikt formale interpretation irgendwie übertrieben ist.
    Für die Domain D nehm ich eine Menge mit möglichst wenigen Elementen (aber natürlich mindestens eins) z.B. D={a,b}
    Meistens reichen ein, zwei oder drei Elemente.
    Den Prädikatsymbolen muss man Mengen zuordnen, z.B. m(A)={a} (A ist ein einstelliges Prädikat) oder m(A)={(a,b)} (A ist ein zweistelliges Prädikat). Diese Mengen können natürlich auch leer sein. Den Konstantensymbolen ordnet m ein Element aus D zu (z.B. m(b)=b), den Funktionssymbolen Funktionen über D (z.B. m(f)(a)=b, m(f)(b)=b).
    Für die freien Variablen definier ich eine assignment, z.B. a(x)=b. Oder ich sag, dass die assignment beliebig sein kann.

  22. #20
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    die Angabe zu Proof Theory wurde am 13.April geändert (nur Anmerkungen hinzugefügt)

  23. #21
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by Dimitrij View Post
    die Angabe zu Proof Theory wurde am 13.April geändert (nur Anmerkungen hinzugefügt)
    Wie definiert man eine Interpretation "in a formal and correct way"?

  24. #22
    Principal
    Join Date
    May 2009
    Posts
    92
    Thanks
    4
    Thanked 13 Times in 12 Posts
    was die formal korrekte interpretation angeht, bin ich jetzt nochmal ins grübeln gekommen.

    wie behandelt man den fall, wenn eine variable gebunden und frei vorkommt?
    normalerweise argumentiert man bei einem forall ja so: This image was created with the kind support of Paulchen

    doch wenn es jetzt schon ein freies x gab, das unter dem assignment zugewiesen wurde, ist diese notation doch problematisch oder? wie kann man das umgehen? eines von beiden x umbenennen?

  25. #23
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Nicht zu kompliziert denken, wie Dimitrij schon geschrieben hat:

    Eine Interpretation ist eine Menge + eine Definition der Relationen und Funktionen bezüglich dieser Menge.
    Man soll bei SAT but not VALID Formeln einfach eine Interpretation angeben unter der die Formel true wird und eine Interpretation unter der die Formel false wird.

    @Adok: Mit dem "define the interpretation in a formal and correct way" ist nur gemeint dass man das ganze mathematisch korrekt (z.B. sind Relationen Subsets vom k-fachen kartesischen Produkt) anschreiben soll.

    @Martin: Du bist anscheinend schon mitten in der semantischen Auswertung der Formeln bezüglich deiner Interpretation - das ist imo garnicht gefordert, man soll die beiden Interpretationen jeweils nur angeben.

  26. #24
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by _m@rt!n View Post
    was die formal korrekte interpretation angeht, bin ich jetzt nochmal ins grübeln gekommen.

    wie behandelt man den fall, wenn eine variable gebunden und frei vorkommt?
    normalerweise argumentiert man bei einem forall ja so: This image was created with the kind support of Paulchen

    doch wenn es jetzt schon ein freies x gab, das unter dem assignment zugewiesen wurde, ist diese notation doch problematisch oder? wie kann man das umgehen? eines von beiden x umbenennen?
    Da gibt es kein Problem. Die Variablenbelegung wird nur für die Formel geändert, die zum Quantor gehört.
    Beispiel:
    Gegeben sei die Formel F, der Frame M und die Variablenbelegung a. Wir wollen den Wahrheitswert berechnen.
    This image was created with the kind support of Paulchen.

    M=(D,m)
    D={0,1}
    m(A)={(0,1),(1,1)}
    m(B)={0}

    This image was created with the kind support of Paulchen

    This image was created with the kind support of Paulchen gdw.
    This image was created with the kind support of Paulchen und This image was created with the kind support of Paulchen.
    Das zweite ist wahr, da a(x)=0 und 0 ist in m(B).
    Das erste ist wahr gdw. This image was created with the kind support of Paulchen für alle This image was created with the kind support of Paulchen.
    This image was created with the kind support of Paulchen wobei a2 diese Belegung ist:
    This image was created with the kind support of Paulchen
    This image was created with the kind support of Paulchen, da a(x)=0 und a(y)=1 und (0,1) ist in m(A)
    This image was created with the kind support of Paulchen, da a2(x)=1 und a2(y)=1 und (1,1) ist in m(A)

    Daher: This image was created with the kind support of Paulchen
    Last edited by Dimitrij; 26-04-2012 at 15:46.

  27. The Following User Says Thank You to Dimitrij For This Useful Post:


  28. #25
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Jetzt stehe ich noch beim Sequenzkalkül #3 beim folgenden Zwischenschritt etwas an:

    This image was created with the kind support of Paulchen

    Angenommen ich mache This image was created with the kind support of Paulchen mit der Wahl This image was created with the kind support of Paulchen - kommt dann This image was created with the kind support of Paulchen oder This image was created with the kind support of Paulchen heraus?

    Ich vermute ersteres, da in This image was created with the kind support of Paulchen noch immer gebundene This image was created with the kind support of Paulchen vorkommen und die durch das This image was created with the kind support of Paulchen nicht verändert werden?

    Anders ausgedrückt geht es mir um die Definition von "bound Variable" bei geschachtelten Quantoren über die gleiche Variable - gilt der Bindingbereich des äußeren Quantors über den ganzen Ausdruck oder nur "bis zum" inneren Quantor?
    Last edited by Raph_M; 26-04-2012 at 21:24.

  29. #26
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Raph_M View Post
    Jetzt stehe ich noch beim Sequenzkalkül #3 beim folgenden Zwischenschritt etwas an:

    This image was created with the kind support of Paulchen
    a ist deine Eigenvariable? Das geht aber nicht. Bei Anwendung einer Regel mit Eigenvariable darf die Eigenvariable im unteren Sequent nicht frei vorkommen. Man weiß aber nicht, ob a in C frei vorkommt. Das weiß man nur von x.

    siehe:
    http://www.cis.upenn.edu/~jean/gbooks/logic.html
    http://sakharov.net/sequent.html

  30. The Following User Says Thank You to Dimitrij For This Useful Post:


  31. #27
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by Dimitrij View Post
    a ist deine Eigenvariable? Das geht aber nicht. Bei Anwendung einer Regel mit Eigenvariable darf die Eigenvariable im unteren Sequent nicht frei vorkommen. Man weiß aber nicht, ob a in C frei vorkommt. Das weiß man nur von x.

    siehe:
    http://www.cis.upenn.edu/~jean/gbooks/logic.html
    http://sakharov.net/sequent.html
    Die Eigenvariable-Condition muss nur berücksichtigt werden, wenn der Allquantor rechts vom \vdash steht. Somit ist OK, was Raph_M gemacht hat. Ich würde auch sagen, Cx bleibt Cx, weil es ja noch an Quantoren gebundene Vorkommnisse von x enthält.

  32. #28
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Adok View Post
    Die Eigenvariable-Condition muss nur berücksichtigt werden, wenn der Allquantor rechts vom \vdash steht.
    Stimmt. Und das A(a) ist ja aus dem forall x A(x) auf der rechten Seite entstanden. Daher ist es nicht korrekt.

  33. #29
    Baccalaureus Adok's Avatar
    Join Date
    Sep 2004
    Location
    Wien
    Posts
    882
    Thanks
    79
    Thanked 76 Times in 66 Posts
    Quote Originally Posted by Dimitrij View Post
    Stimmt. Und das A(a) ist ja aus dem forall x A(x) auf der rechten Seite entstanden. Daher ist es nicht korrekt.
    Wieso? Die Eigenvariable-Bedingung besagt nur, dass die Variable a nicht in der Konklusion stehen darf, wo die Regel \forall r angewandt wurde. In den Prämissen darf sie sehr wohl stehen.

  34. #30
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Adok View Post
    Wieso? Die Eigenvariable-Bedingung besagt nur, dass die Variable a nicht in der Konklusion stehen darf, wo die Regel \forall r angewandt wurde. In den Prämissen darf sie sehr wohl stehen.
    in der Konklusion kommt die Formel C vor, und man weiß nicht, ob C ein freies a enthält

  35. #31
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Danke fürs Durchdenken Dimitrij, die Annahme dass mein geposteter Zwischenschritt durch ein This image was created with the kind support of Paulchen entstanden ist war richtig.

    Wenn ich dich richtig verstehe bedeutet das, dass This image was created with the kind support of Paulchen die einzig gültige Wahl als Eigenvariable für dieses vorhergehende This image was created with the kind support of Paulchen ist, ich dann einfach dieselbe Wahl für das This image was created with the kind support of Paulchen treffe, mein gepostetes Dilemma garnicht auftritt und ich so relativ einfach zu Axiomen komme.

    Aber als abschließende Frage: Ist This image was created with the kind support of Paulchen bei den Quantorenregeln als Ersetzung überhaupt erlaubt (sofern This image was created with the kind support of Paulchen nicht in den anderen Sequenten auftritt)?



    Kleiner edit für die Nachwelt damit jeder versteht worums hier geht und warum die Verwirrung zustande kam:

    Die QuantorenRegeln mit eigenvariable Condition stehen etwas schlecht in den Folien erklärt, z.B. This image was created with the kind support of Paulchen:

    This image was created with the kind support of Paulchen
    ------------------
    This image was created with the kind support of Paulchen

    This image was created with the kind support of Paulchen is an eigenvariable, i.e. This image was created with the kind support of Paulchen <- ungenau!
    This image was created with the kind support of Paulchen is an eigenvariable, i.e. This image was created with the kind support of Paulchen <- besser, free()... freie Variablen im jeweiligen Termset


    Im diskutierten Beispiel ist This image was created with the kind support of Paulchen nicht bekannt, das heisst es kann potenziell jede Variable als freie Variable vorkommen, ausser eben This image was created with the kind support of Paulchen wegen dem Angabetext .
    Last edited by Raph_M; 27-04-2012 at 14:50.

  36. #32
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Raph_M View Post
    Danke fürs Durchdenken Dimitrij, die Annahme dass mein geposteter Zwischenschritt durch ein This image was created with the kind support of Paulchen entstanden ist war richtig.

    Wenn ich dich richtig verstehe bedeutet das, dass This image was created with the kind support of Paulchen die einzig gültige Wahl als Eigenvariable für dieses vorhergehende This image was created with the kind support of Paulchen ist, ich dann einfach dieselbe Wahl für das This image was created with the kind support of Paulchen treffe, mein gepostetes Dilemma garnicht auftritt und ich so relativ einfach zu Axiomen komme.
    genau
    Aber als abschließende Frage: Ist This image was created with the kind support of Paulchen bei den Quantorenregeln als Ersetzung überhaupt erlaubt (sofern This image was created with the kind support of Paulchen nicht in den anderen Sequenten auftritt)?
    ja, ich denk schon.

    Kleiner edit für die Nachwelt damit jeder versteht worums hier geht und warum die Verwirrung zustande kam:

    Die QuantorenRegeln mit eigenvariable Condition stehen etwas schlecht in den Folien erklärt, z.B. This image was created with the kind support of Paulchen:

    This image was created with the kind support of Paulchen
    ------------------
    This image was created with the kind support of Paulchen

    This image was created with the kind support of Paulchen is an eigenvariable, i.e. This image was created with the kind support of Paulchen <- ungenau!
    This image was created with the kind support of Paulchen is an eigenvariable, i.e. This image was created with the kind support of Paulchen <- besser, free()... freie Variablen im jeweiligen Termset
    Beide Bedingungen sind nicht ganz richtig, glaube ich.
    Richtig ist: die Eigenvariable darf in der gesamten Konklusion nicht frei vorkommen, also auch nicht in forall x A. So steht es jedenfalls bei Gallier, bei Sakharov und bei Kleene (Introduction to Metamathematics).
    Im diskutierten Beispiel ist This image was created with the kind support of Paulchen nicht bekannt, das heisst es kann potenziell jede Variable als freie Variable vorkommen, ausser eben This image was created with the kind support of Paulchen wegen dem Angabetext .
    genau
    Last edited by Dimitrij; 27-04-2012 at 15:25.

  37. The Following User Says Thank You to Dimitrij For This Useful Post:


  38. #33
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Dann nochmal danke für die Hilfe, hab deine Anmerkung noch in meinen Post editiert - die Erklärung sollte jetzt komplett richtig sein damit die Anderen nicht in die gleiche Falle wie ich tappen.
    Last edited by Raph_M; 27-04-2012 at 14:55.

  39. #34
    Principal
    Join Date
    Mar 2007
    Posts
    75
    Thanks
    14
    Thanked 4 Times in 2 Posts
    Hi. ich hab bei den natural deductions noch irgendwie probleme. hat vielleicht irgendwer einen link auf ein einfaches durchgerechnetes beispiel? ich konnte keines finden und nur aus den regeln auf den folien werd ich nicht schlau. vielen dank im vorraus

  40. #35
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Seimuun View Post
    Hi. ich hab bei den natural deductions noch irgendwie probleme. hat vielleicht irgendwer einen link auf ein einfaches durchgerechnetes beispiel? ich konnte keines finden und nur aus den regeln auf den folien werd ich nicht schlau. vielen dank im vorraus
    Wir müssen nur bei einer Formel ND anwenden.
    Im Buch Logic in Computer Science (Huth; Ryan) steht viel über Natural Deduction. Im Internet findet man auch einiges. Man kann auch bei Gentzen nachlesen: http://gdz.sub.uni-goettingen.de/dms...g/?IDDOC=17178

  41. #36
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    Wenn 5) valid ist, müsste ich dies doch mit |-F im SC zeigen können. Nachdem ich dann aber die Regeln Exist r und Impl. r angewandt habe, müsste ich Forall r anwenden und eine neue Eigenvariable einführen -> dann komm ich aber auf keine Axiome sondern nur auf Antiaxiome :/

  42. #37
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Deldrarim View Post
    Wenn 5) valid ist, müsste ich dies doch mit |-F im SC zeigen können. Nachdem ich dann aber die Regeln Exist r und Impl. r angewandt habe, müsste ich Forall r anwenden und eine neue Eigenvariable einführen -> dann komm ich aber auf keine Axiome sondern nur auf Antiaxiome :/
    Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.

  43. #38
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    Quote Originally Posted by Dimitrij View Post
    Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.
    oO? Das steht aber hier -> http://www.logic.at/lvas/wiki/images...ooftheory2.pdf nicht !?!? Da wird doch nur als Bedingung bei forall r und exist l angegeben, dass die eingeführte Variable y eine Eigenvariable sein muss.

  44. #39
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Dimitrij View Post
    Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.
    Quote Originally Posted by Deldrarim View Post
    oO? Das steht aber hier -> http://www.logic.at/lvas/wiki/images...ooftheory2.pdf nicht !?!? Da wird doch nur als Bedingung bei forall r und exist l angegeben, dass die eingeführte Variable y eine Eigenvariable sein muss.
    ja eh.
    Ich meinte: nach Anwenden der Regel forall-r wendet man die Regel exist-r an (mit der gleichen Variablenersetzung).

  45. #40
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    Quote Originally Posted by Dimitrij View Post
    ja eh.
    Ich meinte: nach Anwenden der Regel forall-r wendet man die Regel exist-r an (mit der gleichen Variablenersetzung).
    Nur, dass ich Exist r als erstes anwenden muss, da es am äußersten steht.. :/

  46. #41
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Deldrarim View Post
    Nur, dass ich Exist r als erstes anwenden muss, da es am äußersten steht.. :/
    ja, also von unten nach oben betrachtet:
    exist-r
    implication-r
    forall-r
    exist-r
    implication-r

  47. #42
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    Quote Originally Posted by Dimitrij View Post
    ja, also von unten nach oben betrachtet:
    exist-r
    implication-r
    forall-r
    exist-r
    implication-r
    sry, ich steh da irgendwie grad komplett auf der leitung.. wenn ich exist-r und implication-r angewandt habe, hab ich doch keine implication/exists mehr.. dann kann ich nur noch forall anwenden und dann is es aus..

  48. #43
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Der Tipp war schon oben irgendwo - ganz zu Beginn die Formel verdoppeln.

    5) ist das einzige Beispiel wo der Sequenzkalkül nicht "automatisch" aufgeht sondern man etwas tricksen muss .

  49. The Following User Says Thank You to Raph_M For This Useful Post:


  50. #44
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Deldrarim View Post
    sry, ich steh da irgendwie grad komplett auf der leitung.. wenn ich exist-r und implication-r angewandt habe, hab ich doch keine implication/exists mehr.. dann kann ich nur noch forall anwenden und dann is es aus..
    Quote Originally Posted by Raph_M View Post
    Der Tipp war schon oben irgendwo - ganz zu Beginn die Formel verdoppeln.

    5) ist das einzige Beispiel wo der Sequenzkalkül nicht "automatisch" aufgeht sondern man etwas tricksen muss .
    Oder man verwendet die exists-r-Regel, wo die exists-Formel auch oben steht. Das meinte ich, als ich schrieb "Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent".

    Es gibt mindestens zwei Varianten des Sequentialkalküls. Ich glaube, man kann sich aussuchen, welche man für diese Aufgaben verwendet.
    Last edited by Dimitrij; 04-05-2012 at 13:01.

  51. #45
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    ahh.. tricky

  52. #46
    Super Moderator Deldrarim's Avatar
    Join Date
    Mar 2009
    Posts
    1,579
    Thanks
    216
    Thanked 339 Times in 203 Posts
    Quote Originally Posted by Dimitrij View Post
    Oder man verwendet die exists-r-Regel, wo die exists-Formel auch oben steht. Das meinte ich, als ich schrieb "Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent".
    bekomm ich dann nicht nen infinite branch? oder kann ich dann danach einfach die exist regel anwenden, bei der oben kein exist hinkommt?

  53. #47
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Deldrarim View Post
    bekomm ich dann nicht nen infinite branch?
    nein
    Man erhält dann eh ein Axiom (ein Sequent, wo die linke und die rechte Seite eine Formel gemeinsam haben).
    oder kann ich dann danach einfach die exist regel anwenden, bei der oben kein exist hinkommt?
    Naja, dann würde man die Varianten des Sequentialkalküls vermischen. Ich weiß nicht, ob man das darf/soll.

    Die eine Variante des Sequentialkalküls stammt von Gentzen (in den Folien: LK):
    http://sakharov.net/sequent.html
    Das ist eine zweite Variante (G4 von Kleene; in den Folien: LK'; ich verwende diese; wird auch in TIL verwendet, aber nur für Aussagenlogik):
    http://sakharov.net/sequent.html#formulation
    Last edited by Dimitrij; 04-05-2012 at 15:30.

  54. The Following User Says Thank You to Dimitrij For This Useful Post:


  55. #48
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Quote Originally Posted by Dimitrij[/QUOTE
    Es gibt mindestens zwei Varianten des Sequentialkalküls. Ich glaube, man kann sich aussuchen, welche man für diese Aufgaben verwendet.

    Stimmt, in den Folien sind auch beide Varianten.

  56. #49
    Principal
    Join Date
    Dec 2007
    Posts
    64
    Thanks
    5
    Thanked 7 Times in 7 Posts
    Bin grad am übertragen der aufgabe in Latex, wie formatiert ihr das ganze? Speziell, tragt ihr bei jedem step die zugehörige regel ein?
    oder reicht das hier (Aufgabe1, SC):
    Attached Thumbnails Attached Thumbnails Click image for larger version. 

Name:	formating.png 
Views:	25 
Size:	34.2 KB 
ID:	20867  

  57. #50
    Hero
    Join Date
    Nov 2008
    Posts
    186
    Thanks
    15
    Thanked 34 Times in 26 Posts
    Ist das "manuell" erstellt?

    Mit http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/ gehts sehr komfortabl, z.B. werden die Sequenzsymbole ausgerichtet und man kann auch die Regeln seitlich annotieren (wie ist im Manual auf der Seite sehr gut beschrieben).

    Ah und weil ichs grad seh - die This image was created with the kind support of Paulchen und This image was created with the kind support of Paulchen sind überflüssig.
    Last edited by Raph_M; 04-05-2012 at 17:31.

  58. The Following User Says Thank You to Raph_M For This Useful Post:


  59. #51
    Hero Madnebular's Avatar
    Join Date
    Dec 2008
    Location
    Vienna
    Posts
    213
    Thanks
    41
    Thanked 43 Times in 24 Posts
    Quote Originally Posted by daLois View Post
    Bin grad am übertragen der aufgabe in Latex, wie formatiert ihr das ganze? Speziell, tragt ihr bei jedem step die zugehörige regel ein?
    oder reicht das hier (Aufgabe1, SC):
    Braucht man das Gamma und Delta bei uns? Dachte die wären leere Mengen.

    Außerdem hätt ich noch eine Frage zur Natural Deduction, das mir iwie nicht einleuchtet... Bei Beispiel 5 müssen wir ja " |- ! phi " zeigen. Und kann ich dann nicht einfach die Assumption " phi " treffen, daraus Falsum ableiten, und dann beweisen wie ich lustig bin? Das kommt mir halt relativ spanisch vor...
    der "thanks" button ist dazu da ihn zu benutzen. also spart euch die zeit danke schreiben zu müssen und drückt halt drauf

  60. #52
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Madnebular View Post
    Braucht man das Gamma und Delta bei uns? Dachte die wären leere Mengen.
    stimmt
    Außerdem hätt ich noch eine Frage zur Natural Deduction, das mir iwie nicht einleuchtet... Bei Beispiel 5 müssen wir ja " |- ! phi " zeigen. Und kann ich dann nicht einfach die Assumption " phi " treffen, daraus Falsum ableiten, und dann beweisen wie ich lustig bin? Das kommt mir halt relativ spanisch vor...
    Bei Beispiel 5 brauchen wir nicht ND machen, da die Formel gültig ist.

  61. #53
    Hero Madnebular's Avatar
    Join Date
    Dec 2008
    Location
    Vienna
    Posts
    213
    Thanks
    41
    Thanked 43 Times in 24 Posts
    Quote Originally Posted by Dimitrij View Post
    stimmt


    Bei Beispiel 5 brauchen wir nicht ND machen, da die Formel gültig ist.
    Ich meinte eh 1. Man nimmt ja die negierte Formel an. Und nachdem man ja sonst keine Formeln zum Arbeiten hat, muss man was annehmen. Also hab ich die ursprüngliche Formel angenommen. Und damit hab ich schon mein Falsum. Kann mich bitte jemand kurz aufklären? Ich hab das Gefühl ich überseh da was.
    der "thanks" button ist dazu da ihn zu benutzen. also spart euch die zeit danke schreiben zu müssen und drückt halt drauf

  62. #54
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Madnebular View Post
    Ich meinte eh 1. Man nimmt ja die negierte Formel an. Und nachdem man ja sonst keine Formeln zum Arbeiten hat, muss man was annehmen. Also hab ich die ursprüngliche Formel angenommen. Und damit hab ich schon mein Falsum.
    Wieso hast du damit schon ein Falsum? Das musst du ja erst ableiten.

  63. #55
    Hero Madnebular's Avatar
    Join Date
    Dec 2008
    Location
    Vienna
    Posts
    213
    Thanks
    41
    Thanked 43 Times in 24 Posts
    Ergibt sich das nicht sofort aus der Assumption von phi? Phi, !phi |- Falsum?
    Oder funktioniert das eher so?

    1. !phi prämisse
    2. phi assumption
    4. phi[x/b] forall e 2
    5. r(b,b) > !r(b,b) and e_1 4
    6. r(b,b) assumption
    7. !r(b,b) > e 5
    8. Falsum !e 6,7

    Mir ist das halt nicht wirklich klar wann ich was annehmen darf, und wie sich das auswirkt, weil das in den Folien nicht wirklich vorkommt...


    Nicht? Das ist eben das, was ich nicht verstehe...
    der "thanks" button ist dazu da ihn zu benutzen. also spart euch die zeit danke schreiben zu müssen und drückt halt drauf

  64. #56
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Madnebular View Post
    Ergibt sich das nicht sofort aus der Assumption von phi? Phi, !phi |- Falsum?
    Oder funktioniert das eher so?

    1. !phi prämisse
    2. phi assumption
    4. phi[x/b] forall e 2
    5. r(b,b) > !r(b,b) and e_1 4
    6. r(b,b) assumption
    7. !r(b,b) > e 5
    8. Falsum !e 6,7

    Mir ist das halt nicht wirklich klar wann ich was annehmen darf, und wie sich das auswirkt, weil das in den Folien nicht wirklich vorkommt...


    Nicht? Das ist eben das, was ich nicht verstehe...
    !phi ist keine Prämisse. Man muss !phi herleiten, ohne irgendwelche Prämissen.

  65. #57
    Hero Madnebular's Avatar
    Join Date
    Dec 2008
    Location
    Vienna
    Posts
    213
    Thanks
    41
    Thanked 43 Times in 24 Posts
    Quote Originally Posted by Dimitrij View Post
    !phi ist keine Prämisse. Man muss !phi herleiten, ohne irgendwelche Prämissen.
    Dh ich muss |- !phi aus |- phi herleiten?
    der "thanks" button ist dazu da ihn zu benutzen. also spart euch die zeit danke schreiben zu müssen und drückt halt drauf

  66. #58
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by Madnebular View Post
    Dh ich muss |- !phi aus |- phi herleiten?
    Du musst !phi aus nichts herleiten. Du darfst aber Annahmen treffen, die du dann wieder aufhebst durch passende Regelanwendungen.

  67. #59
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    verbale Kurzfassung des ND-Beweises von Beispiel 1:
    Angenommen, die Formel aus Beispiel 1 wäre wahr (in einer Interpretation). Dann lässt sich herleiten, dass -R(b,b) wahr ist. Dann lässt sich auch herleiten, dass R(b,b) wahr ist. Widerspruch! Also ist die Formel nicht wahr.

  68. The Following 2 Users Say Thank You to Dimitrij For This Useful Post:


Bookmarks

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •