KeY - Bug?

hstr
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

KeY - Bug?

Beitrag von hstr »

Hallo,
ich versuche gerade Problem 1, Aufgabe a.) in KeY zu beweisen. Das funktioniert auch bis zu orLeft Regel,
aber dann müsste man ja für jeden der beiden Zweige die allLeft Regel anwenden, was aber nicht funktioniert.
Sobald man auf "\forall s x; p(x)" geht und "allLeft" auswählt, wird der ganze Proof Tree ausgegraut und man kann fast überhaupt nichts mehr machen.
(auch kein "Goal Back")
Interessanterweise funktioniert der Beweis aber mit dem automated proof search, obwohl der genau die gleichen Schritte ausführt.
Was läuft da schief?

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

Re: KeY - Bug?

Beitrag von Nathan Wasser »

Es gab auf der Seite "Links, Papers, and Software" leider zwei verschiede Links zum KeY Tool, wobei nur eine korrekt funktioniert. Die Links zeigen nun beide auf die korrekte Version.

hstr
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Re: KeY - Bug?

Beitrag von hstr »

Ich habe die neuste Version von key-project.org verwendet.

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

Re: KeY - Bug?

Beitrag von Nathan Wasser »

Das ist aber nicht die Version, die für FGdI3 verwendet werden soll.

Antworten

Zurück zu „Archiv“