Sequentialkalkül
Results 1 to 6 of 6
  1. #1
    Zentor's Avatar
    Title
    CO-Administrator
    Join Date
    Dec 2001
    Location
    Wien???
    Posts
    1,156
    Thanks
    2
    Thanked 9 Times in 6 Posts

    Unhappy Sequentialkalkül

    Ich hab da ein Problem mit dem Bsp 4.31 zum Sequenzialkalkül auf der Seite 72. Wieso kann man für
    A impliziert B, A |-- B die Formel impliziert-L anwenden?
    die heißt
    F,A impliziert B |-- G
    Wenn ich jetzt {A} als F und {B} als G annehm schaut das wie
    A, A impliziert B |-- B
    aus und nicht
    A impliziert B, A |-- B
    ???
    Das ist doch nicht equivalent oder?
    mfg Zentor

  2. #2
    shabby's Avatar
    Title
    Elite
    Join Date
    Jan 2002
    Location
    Schrödinger, 1040 Wien
    Posts
    267
    Thanks
    2
    Thanked 9 Times in 8 Posts
    Doch das ist äquivalent

    F|--G mit F={F1,..Fn},G={G1,..,Gn} bedeutet
    sind F1,F2,..,Fn in allen Interpretatationen war, dann ist mindestens ein Gi war
    da wir in G nur einen Sequent haben, heißt das:
    Semantisch: Wenn alle Fi war sind, ist G war
    Syntaktisch F1^F2^..^Fn wahr, dann G war
    Ich nehme an du könntest irgendwie auch eine Implikation hinschreiben, aber aus mir bisher unerfindlichen Gründen, schränkt das die Allgemeinheit ein, d.h. ich glaube im Allgemeinen sind "impliziert" und "läßt sich ableiten aus" nicht ident.
    ABER: Im Speziellen ist die UND-Verknüpfung kommutativ, sicher aber die Menge der Formeln in F, weil es ja egal ist ob ich "Sind F1 und F2 wahr" oder "Sind F2 und F1 wahr" meine.

    btw: wie in vielen anderen Fächern auch (Paradebeispiel: Mathe), ist es auch in TheoInf für uns, die die Tiefen der Logik nicht kennen, nicht leicht ersichtlich, warum viele anscheinend logisch klingende Sachen im Allgemeinen nicht gültig sind (Vektorräume !)
    Last edited by shabby; 25-06-2002 at 21:47.

  3. #3
    Zentor's Avatar
    Title
    CO-Administrator
    Join Date
    Dec 2001
    Location
    Wien???
    Posts
    1,156
    Thanks
    2
    Thanked 9 Times in 6 Posts
    Was bedeutet dann F, A ??
    und wo ist der Unterschied zwischen F,G und A,B in den Formeln?
    Wie kann man dann schlussendlich sagen das die Gesamtformel ableitbar ist, müssen alle Variablen je links und rechts von |-- zu finden sein?
    mfg Zentor

  4. #4
    shabby's Avatar
    Title
    Elite
    Join Date
    Jan 2002
    Location
    Schrödinger, 1040 Wien
    Posts
    267
    Thanks
    2
    Thanked 9 Times in 8 Posts
    1)

    F,G sind Mengen von Formeln
    A,B sind einzelne Formeln

    F,A |-- B bedeutet:

    F1,F2,..Fn,A |-- B wobei wir aber die Fi Formeln zu einer Zusammenfassen, weil sie uns im entsprechenden Axiom nicht interessieren. zum Beispiel

    die NOT(l) - Ableitung:

    F,not B |-- G ===> F |-- G,A

    bedeutet

    wenn wir auf der linken Seite eine endliche Menge von Formeln haben, von den EINE SPEZIELLE not B ist (der Rest ist uns Egal), dann können wir sie von der linken Formelmenge weggeben und zur rechten in nicht-negierter Form dazu (informell gesprochen)

    2)
    Die Ableitung ist gültig wenn am Ende nur Axiome in den obersten Ableitungen stehen. (einziges Axiom des SeqKalküls: Wenn es Formeln gibt, die links und rechts von |-- vorkommen dann folgt daraus -> F |-- G)

    Ähmm, mit einem Wort: so isses.
    Last edited by shabby; 25-06-2002 at 23:19.

  5. #5

    Title
    Veteran
    Join Date
    Mar 2002
    Posts
    13
    Thanks
    0
    Thanked 0 Times in 0 Posts
    ableitbar is es dann wenn links und rechts von |-- ein und die selbe variable vorkommt

    A|--A,B ist ableitbar weil A links und rechts von dem haxn steht.

    ich hab aber auch probleme mit der implikation links bei bsp 4.31

    und bei oder links bei bsp 4.32 1. Variante
    die 2. ist sonnenklar

    ich hätt ma dacht dass das so ausschaut

    A v B, not A |--b

    B,not A ist B
    b ist G
    A ist A

    aber was ist dann F?

    so kanns ja wohl net stimmen weil ich so net weiterkomm

  6. #6

    Title
    Veteran
    Join Date
    Mar 2002
    Posts
    13
    Thanks
    0
    Thanked 0 Times in 0 Posts
    sorry! wollte keine verwirrung stiften! Problem ist gelöst!

    is ja wurscht wie ichs anschreibt

    zu Bsp 4.31

    A impliziert B, A |-- B is ja das selbe wie A, A impliziert B |--B

    und dann passt eh eins zu eins mit implikation links zusammen

    und zu Bsp 4.32

    A v B, not A |-- B is das selbe wie not A, A v B |--B und dann passts eins zu eins zu oder links

    vielleicht konnte ich damit auch zentor helfen mit dem was ist F und G Problem

    funky

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
  •