Lab 3 - Sequenzenkalkül

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Lab 3 - Sequenzenkalkül

Beitrag von null »

Hallo zusammen,

ich habe zwei Fragen bezüglich des Beweises im Sequenzenkalkül, den wir im dritten Lab durchführen müssen.

1.) Vielleicht ist die Frage ein bisschen doof, aber wo ist die linke und wo die rechte Seite? Auf den verlinkten Regeln wird durch einen Doppelpfeil immer klar, linke und rechte Seite getrennt. In der gegebenen Formel kann ich diesen nicht finden. Da die Formel ja anscheinend nicht allgemeingültig ist, steht nicht alles auf der rechten Seite.

2.) Falls wir auf der linken Seite den Allquantor oder auf der rechten den Existenzquantor eliminieren wollen, müssen wir diese laut Regel mit uns ziehen. In FGDI2 durften wir zur besseren Lesbarkeit die Quantoren dann weglassen. Dürfen wir das hier auch?

Vielen Dank
null

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab 3 - Sequenzenkalkül

Beitrag von JannikV »

Zu 1. Also so wie ich das sehe ist die Formel schon allgemeingültig und zu aller erst steht nichts auf der linken Seite. Dann wendet man die Regel Implikation rechts an und schafft den Teil links vom \(\rightarrow\) auf die linke Seite vom \(\Rightarrow\).

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Lab 3 - Sequenzenkalkül

Beitrag von null »

Falls eine Formel allgemeingültig ist, so haben wir in FGDI 2 immer den Doppelpfeil ganz nach links geschrieben, also mit einer leeren linken Seite. Aus der Aufgabenstellung kann man ja nicht herauslesen, dass sie allgemeingültig ist. Da steht nur, dass wir die "validity" nachprüfen sollen. Das könnte doch auch "erfüllbar" heißen, oder?

Viele Grüße

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Lab 3 - Sequenzenkalkül

Beitrag von yourmaninamsterdam »

"Valid" heißt "allgemeingültig". Erfüllbarkeit heißt auf Englisch "satisfiability".

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Lab 3 - Sequenzenkalkül

Beitrag von null »

Hallo,

vielen Dank für die Antwort. Damit ist es für mich klarer geworden.

Ich möchte nun die Aufgabe sowohl per Hand als auch mittels Key lösen. Beim Key System ist mir jedoch eine Sache nicht so ganz klar. Ich möchte \(\exists\) left side anwenden. Dazu wird für die quantifizierten Variabeln eine Konstante eingesetzt. Eigentlich nichts Schwieriges. Key jedoch bietet mir zwei Möglichkeiten an:

1.) cut_direct: Das führt dazu, dass anstatt des Existenzausdrucks, true hingeschrieben wird. Wie Key darauf kommt, weiß ich nicht.

2.) local_cut: Diese Option muss wohl verwendet werden. Ich schaffe es jedoch nicht, die quantifizierte Variabel x durch eine Konstante c zu ersetzen. Logischerweise ist c noch nicht in der .key Datei deklariert, da ich ja noch nicht wissen kann, welche Variabeln ich später mal brauche.

Kann mir jemand sagen, wie ich diese Ersetzung in Key vornehme?

Herzlichen Dank
LG, null

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: Lab 3 - Sequenzenkalkül

Beitrag von errt »

Du hast wahrscheinlich den falschen Ausdruck markiert. Um exists_left anwenden zu können (was das ist, was du suchst), musst du das exists selbst markieren, nicht z.B. nur den quatifizierten Term.

studypad
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 158
Registriert: 30. Mär 2011 11:46

Re: Lab 3 - Sequenzenkalkül

Beitrag von studypad »

Bei \(\forall\) left side wird ja eine mögliche Instanziierung mit gewollten Buchstaben genommen und das \(\forall\) nochmal dazu geschrieben. Dürfen wir es dann, wenn es uns nur "Platz" raubt, auch weglassen?

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

Re: Lab 3 - Sequenzenkalkül

Beitrag von Nathan Wasser »

studypad hat geschrieben:Bei \(\forall\) left side wird ja eine mögliche Instanziierung mit gewollten Buchstaben genommen und das \(\forall\) nochmal dazu geschrieben. Dürfen wir es dann, wenn es uns nur "Platz" raubt, auch weglassen?
Nein, weglassen dürft ihr es nicht.

Ihr dürft aber einen für den Beweis nie mehr auch nur im geringsten benötigten Teil mit "..." abkürzen. Es muss klar sein, dass hier was steht und ihr lediglich Platz und Schreibarbeit sparen wollt und nicht, dass ihr die Regel falsch angewendet habt. Ausserdem darf an keiner Stelle aus dem "..." plötzlich wieder magisch etwas entstehen, weil ihr bemerkt habt, dass ihr es doch noch benötigt. Im Zweifel daher lieber alles aufschreiben.

ez22
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 28. Mär 2011 14:52

Re: Lab 3 - Sequenzenkalkül

Beitrag von ez22 »

wenn ein Close bei der Auswahl der Kalkülgereln gibt, heißt es, dass die linke Seite die rechte Seite schon erfüllt?
Vielen Dank

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

Re: Lab 3 - Sequenzenkalkül

Beitrag von Nathan Wasser »

ez22 hat geschrieben:wenn ein Close bei der Auswahl der Kalkülgereln gibt, heißt es, dass die linke Seite die rechte Seite schon erfüllt?
Vielen Dank
Es bedeutet, dass die Regel "Close" anwendbar ist. Also ja, die rechte Seite folgt trivial aus der linken Seite, da eines der (UND-verketteten) Elemente links auch in der (ODER-verketteten) rechten Seite vorkommt.

Antworten

Zurück zu „Archiv“