Announcement

Collapse
No announcement yet.

Übung Proof Theory

Collapse
X
  • Filter
  • Time
  • Show
Clear All
new 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
    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.

    Comment


    • #3
      Mir ist noch etwas eingefallen: "Negation Allquantor" entspricht ja "Existenzquantor Negation". Vielleicht hilft dir diese Regel beim Natural-Deduction-Beispiel.

      Comment


      • #4
        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...

        Comment


        • #5
          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.

          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?

          Comment


          • #6
            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.

            Comment


            • #7
              bussproofs ist gut geeigent:
              http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/

              Comment


              • #8
                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.

                Comment


                • #9
                  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, 22:41. Reason: natürlich die mit eugenvariable nicht die ohne

                  Comment


                  • #10
                    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.

                    Comment


                    • #11
                      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, 11:06.

                      Comment


                      • #12
                        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)

                        Comment


                        • #13
                          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?

                          Comment


                          • #14
                            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.

                            Comment


                            • #15
                              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.

                              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

                              Comment

                              Working...
                              X