3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

ic89dixy
Erstie
Erstie
Beiträge: 12
Registriert: 15. Okt 2012 18:07

3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von ic89dixy » 10. Feb 2014 21:15

Wenn ich die Regel allLeft oder existsLeft anwenden will verlangt KEY von mir die Eingabe eines t( G term). Leider reicht mein Verständnis nicht aus um herauszufinden was das bedeutet oder was ich hier eingeben soll damit die Regel anwendbar ist.
Bitte um Hilfe

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von rindphi » 10. Feb 2014 21:53

Deine Frage lässt sich auf den weniger komplexen Sequenzenkalkül aus den Vorlesungen reduzieren. Zuerst einmal etwas Grundsätzliches zum Umgang mit Quantoren im Kalkül:
  • Regel allRight: Allaussage \(\forall x. \phi(x)\) auf der rechten Seite. Du sollst eine Aussage für alle möglichen Werte einer Variablen zeigen. Das ist, gemäß dem altbekannten "sei x fix, aber beliebig" equivalent zum Beweis der Aussage für eine frische Konstante. Du kannst \(\forall x. \phi(x)\) also ersetzen durch \(\phi(c)\) für irgendeine neue Konstante c. KeY wird dir hier automatisch eine generieren, du musst keine Eingabe tätigen.
  • Regel exLeft: Existenzaussage \(\exists x. \phi(x)\) auf der linken Seite. Du kannst davon ausgehen, dass es ein x gibt, sodass \(\phi(x)\) gilt. Mehr weißt du allerdings nicht über dieses x. Um trotzdem mit diesem Wissen arbeiten zu können, kannst du \(\exists x. \phi(x)\) ersetzen durch \(\phi(c)\) für irgendeine neue Konstante c. KeY wird dir hier wieder automatisch eine generieren. Du weißt zwar noch nichts über c, aber immerhin, es gibt einen solchen "Zeugen" für deine Formel. In diesem wie auch im letzten Fall brauchen wir die ursprüngliche Teilformel nicht mehr, da die Aussagen für eine frische Konstante äquivalent sind!
  • Regel exRight: Existenzaussage \(\exists x. \phi(x)\) auf der rechten Seite. Du sollst zeigen, dass es irgendein x gibt, für das \(\phi(x)\) gilt. Es reicht wirklich, irgendeines zu finden, du kannst also frei wählen! Um das richtige zu wählen, musst du dir über die Bedeutung der zu zeigenden Gesamtaussage klar werden, bzw. so wählen, dass du letztendlich den Beweis mit der Regel Close schließen kannst. Es geht darum, das gleiche Atom auf jede Seite der Sequenz zu bekommen. Falls du einen nicht zielführenden Term gewählt hast, kannst du es beliebig oft noch einmal probieren; aus diesem Grund darf die ursprüngliche Aussage \(\exists x. \phi(x)\) auch nicht gelöscht werden. Der Kalkül bleibt damit "konfluent".
  • Regel allLeft: Allaussage \(\forall x. \phi(x)\) auf der linken Seite. Das ist der für dich interessante Fall. Du weißt etwas, nämlich \(\phi(x)\), für alle möglichen x. Du kannst dieses Wissen also für jeden beliebigen Term deiner Wahl nutzen. Welche Terme das sind, hängt vom spezifischen Problem ab. Ansonsten gelten die Anmerkungen zu exRight.
Wenn KeY also bei allLeft einen Term verlangt (bei exLeft wird es das nicht tun), dann hängt es vom Problem ab, welcher Term da zielführend ist. Grundsätzlich ist ein Term immer eine Konstante, oder ein Funktionssymbol angewendet auf andere Terme (siehe Folien). Bei Beweisen mit Java ist außerdem self (repräsentiert Java's "this") ein Term sowie alle Ausdrücke der Art self.field, self.field.value etc., wobei field ein Feld des aktuellen Objekts und value ein Wert davon ist. Das Termmaterial baut sich also üblicherweise aus solchen self-Ausdrücken (etc.) und aus den bisher eingeführten frischen Konstanten auf (und das darfst du legalerweise im Eingabefeld in KeY auch eingeben). Falls Funktionssymbole vorhanden sind, wird die Termmenge unendlich groß, sonst bleibt sie endlich und es sollte sogar theoretisch möglich sein, alle Werte auszuprobieren.

Das Problem des Findens eines passenden Terms ist übrigens DAS Problem überhaupt in Logik erster Stufe. Ansonsten wäre diese nach dem Satz von Herbrand entscheidbar und KeY würde potenziell gar keine Interaktion mehr benötigen. Nach Church/Turing, die die Unentscheidbarkeit zeigten, kann man diese Hoffnung allerdings abschreiben. Du hast also gerade quasi des Pudels Kern entdeckt ;)

Hoffe, ich konnte irgendwie weiterhelfen.

ic89dixy
Erstie
Erstie
Beiträge: 12
Registriert: 15. Okt 2012 18:07

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von ic89dixy » 11. Feb 2014 19:16

Vielen Dank für die Ausführliche Antwort. Auch wenn ich das noch nicht ganz verstehe hat es mir etwas geholfen. :-)

firefluxx
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 12. Feb 2014 14:55

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von firefluxx » 12. Feb 2014 14:58

Hey,

ich bekomme es leider trotz dem ausführlichen Beitrag nicht hin, in KeY solch einen Term zu schreiben. Bin mir auch alles andere als sicher (d.h. ich habe keine Ahnung) WO dieser Term denn dann stehen sollte (nur in der Eingabemaske? Oder [auch] in der Datei?) und wie er auszusehen hat...

Hat jemand da ne Ahnung?

randall
Neuling
Neuling
Beiträge: 3
Registriert: 22. Okt 2013 22:53

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von randall » 12. Feb 2014 16:09

Hi,
ich habe da auch nicht so viel Ahnung, aber vielleicht hilft es ja.
Also um diesen Term zu beschreiben benötigst du zu erst eine Konstante. Entweder eine selbstdefinierte oder du wendest zuerst eine allright- oder exleft-regel an - da generiert dir
Key automatisch eine. Diese Konstante kannst du nun in deinem Term nutzen
Sei "c" eine solche Konstante
der verlangte G term zumindest bei mir lautete dann in etwa: {\subst s x;c}c
Was so viel heisst wie x vom Typ s wird mit dem Symbol c ersetzt und c wird dann als Substitution eingesetzt.

In KEY
Ungeachtet der Einfachheit des Beispiels:
\exists s x; r(x) -> \exists s x; r(x)

exleft
r(c) -> \exists s x; r(x)

exright (diese Substitiutionsformel erstellen)
r(c) -> r( {\subst s x;c}c) , \exists s x; r(x)

applySubst.
r(c) -> r(c), \exists s x; r(x)

Ich hoffe das ist nicht falsch und nachvollziehbar

LG

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von Nathan Wasser » 12. Feb 2014 16:25

Zu erwähnen ist vielleicht noch, dass bei der Wahl des Terms bei allLeft und exRight nicht zwingend ein Konstantensymbol ("c") gewählt werden muss, sondern es reicht ein variablenfreier Term. Dieser ist natürlich auch konstant, aber ich betone einfach mal, dass es sich durchaus um einen größeren Term handeln kann.

Zum Beispiel benötigt man dies um folgendes zu beweisen (wir nehmen an es gäbe kein Integeroverflow):

\(\Longrightarrow \forall \ int \ x; \exists \ int \ y; x < y\)

Zuerst benutzen wir allRight mit einer frischen Konstante "c":

\(\Longrightarrow \exists \ int \ y; c < y\)

Dann benutzen wir exRight mit dem variablenfreien Term "c + 1":

\(\Longrightarrow c < c + 1, \exists \ int \ y; c < y\)

firefluxx
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 12. Feb 2014 14:55

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von firefluxx » 12. Feb 2014 16:34

:shock: :idea:

Danke Randall für deine Antwort! Super verständlich, jetzt weiß ich auch endlich, wie ich das in KeY anwenden muss. Das hat mir definitiv weitergeholfen! :) :)

@Nathan: Danke trotzdem für den Versuch, wie auch immer ich das anwenden kann...

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

Re: 3.1 Proof mit allLeft oder existsLeft -> t( G term) ????

Beitrag von rindphi » 14. Feb 2014 12:39

An sich ist es nicht schwer, einen Term einzugeben. Das zuständige Eingabefeld ist im folgenden Screenshot markiert:

Bild

Es handelt bei dem abfotografierten Beispiel um das vierte Problem in der 4. Übung. Der Term "a" ist hier auch die Lösung.
Etwas wie " {\subst s x;c}c " muss nie eingegeben werden. In diesem Fall wäre die Eingabe "c" in das oben markierte Feld.

Antworten

Zurück zu „Archiv“