Frage zu 8.2 b)

NonStop
Mausschubser
Mausschubser
Beiträge: 73
Registriert: 18. Apr 2015 19:15

Frage zu 8.2 b)

Beitrag von NonStop »

Die Aufgabe ist ja, eine Kalkülregel zu definieren, sodass man die gleichen Urteile, wie vor dem Entfernen der Regeln aror1 und aror2 herleiten kann.
Mit der Regel aror1 könnte man trivialerweise folgendes Urteil herleiten:
<(true or not true), sigma> ->1 true

Wie kann man dieses Urteil denn mit den 4 in dem Aufgabenteil hinzugefügten und der in der MuLö vorgestellten Regeln herleiten?
aror5' lässt sich hier nicht anwenden, da true nach dem Pfeil nicht die Form (b1 or b2') hat, Wenn ich die Regel richtig verstehe :D

FlorianD
Mausschubser
Mausschubser
Beiträge: 92
Registriert: 14. Jan 2015 17:25

Re: Frage zu 8.2 b)

Beitrag von FlorianD »

Um eine der neuen Regeln anzuwenden, musst du lediglich (true or not true) zu (true or false) umformen. Das geht mit Regel \(ar\vee5'\). Es ist \(b_1 = true\), \(b_2= not~ true\), also auch \(b_2 \notin Bool\), weshalb die Regel angewendet werden kann.

Edit: Habe das Problem falsch verstanden, du könntest recht haben

Grüße
Florian

Antworten

Zurück zu „Archiv“