Äquivalenz zweier Programmen

trojan
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 12. Jun 2011 23:03

Äquivalenz zweier Programmen

Beitrag von trojan »

Hallo,
es soll gezeigt werden, dass die Programme äquivalent sind:
scr.jpg
scr.jpg (24.2 KiB) 364 mal betrachtet
Ich will nun die Richtung => beweisen:
Fall 1) wenn die letzte Regel rift ist, habe ich bereits bewiesen
Fall 2) die letzte Regel ist riff. Dann haben wir in Prämissen zwei Teilen, nämlich
((x = x), sigma) => false (skip, sigma) => sigma'

Meine Frage ist, was wir mit ((x = x), sigma) => false weiter machen? x = x kann ja nie false sein, also sollte es eigentlich keine Herleitung dafür geben, stimmt das?
Grüße

Alby407
Mausschubser
Mausschubser
Beiträge: 64
Registriert: 19. Jul 2014 15:40

Re: Äquivalenz zweier Programmen

Beitrag von Alby407 »

Also meiner Meinung nach kann die letzte Instanz nur die Regel rift sein, weil rein logisch ja x=x immer gilt. Da könnte genauso true stehen :?
Ich würde jetzt auch sagen, dass es keine Herleitung dafür gibt.

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

Re: Äquivalenz zweier Programmen

Beitrag von FlorianD »

Hallo,

du kannst den Fall zu einem Widerspruch führen und damit zeigen, dass dieser Fall nicht möglich ist. Das wurde zum Beispiel in 6.3 Fall 2a gemacht.

Grüße
Florian

trojan
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 12. Jun 2011 23:03

Re: Äquivalenz zweier Programmen

Beitrag von trojan »

Stimmt, habs übersehen, danke!

Antworten

Zurück zu „Archiv“