Seite 1 von 1

KeY - Bug?

Verfasst: 20. Dez 2012 09:41
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?

Re: KeY - Bug?

Verfasst: 20. Dez 2012 12:21
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.

Re: KeY - Bug?

Verfasst: 20. Dez 2012 13:55
von hstr
Ich habe die neuste Version von key-project.org verwendet.

Re: KeY - Bug?

Verfasst: 20. Dez 2012 14:26
von Nathan Wasser
Das ist aber nicht die Version, die für FGdI3 verwendet werden soll.