Übung 8 Aufgabe 1.2

[danny]

In Aufgabenteil 2 von Aufgabe 1 werden ja die Regeln (ar∨1) und (ar∨2) aus dem Kalkül heraus genommen. Mit Hilfe der Regel (ar∨1) konnte man beispielsweise folgende Herleitung hinschreiben:

Code: Alles auswählen

(ar∨1) -----------------------------
        <true ∨ ¬false, σ> ->1 true

Mit den vier neu eingeführten Regeln zusammen mit der aus der Musterlösung anstatt (ar∨1) und (ar∨2) ist eine Herleitung dieses Urteils jedoch nicht mehr möglich, oder übersehe ich da was?

[dees]

Das siehst du richtig und ist genau der Grund warum du in der Aufgabe noch eine Regel angeben sollst. Und dann kannst du auch diesen Typ von Konklusion herleiten.

gruß

[danny]

Die neu eingeführte Regel aus der Musterlösung habe ich bereits in meine Betrachtungen mit einbezogen. Aber auch zusammen mit der scheint es nicht möglich zu sein, folgendes Urteil herzuleiten:

Code: Alles auswählen

<true ∨ ¬false, σ> ->1 true

Also ist entweder die Musterlösung falsch, oder ich übersehe, wie man die neuen Regeln so anwenden kann, dass sich dieses Urteil herleiten lässt.

[mansur]

(ar ∨ 1) ist aber das hier:
⟨true ∨ b_2, σ⟩ →1 true

und nicht das was du im ersten beitrag geschrieben hast... oder seh ich da was falsch?

[danny]

Du kannst b_2 ja aber als ¬false wählen (ist ja aus Bexp)

Somit kann man mit Hilfe der Regel (ar∨1) das Urteil aus dem Ursprungspost herleiten, oder.

[MaMaj]

Hmm?

Die neu eingeführte Regel ist doch (ar∨5′)... und da ist b 2 doch gerade KEIN Element der TRUTH-Menge... also irgendwas verstehe ich auch gerade nicht...

EDIT: Ah, kein true, oder false... aber eine Bexp... ja, dann macht es Sinn: Die Prämisse ist ja dann ⟨b2,σ⟩ →1 b′2 mit b2 z.B. "true ∨ Bexp"

EDIT2: kein true, oder false ist natürlich nicht ganz richtig! Besser: b2 element Bexp \ T. Oder?