Verwendung von Linearer Arithmetik in einem automatischen Induktionsbeweiser

 

Thomas Dickmeis

 

Abstract:

 

 

 Das Verifikationsprogramm AProVE des LuFGI2 ist nicht nur zur
Untersuchung der Terminierung bestens geeignet, sondern es verfügt auch
über einen automatischen Induktionsbeweiser für partielle
Korrektheitsaussagen.
Bisher werden Beweise nur anhand syntaktischer Merkmale geführt.
Vorhandenes semantisches Wissen wird dabei jedoch nicht berücksichtigt.
Dies führt dazu, dass für vermeintlich einfache Aussagen die Beweise,
sofern sie mit dieser Einschränkung gefunden werden, länger und
schwieriger nachzuvollziehen sind.

Daher ist es die Zielsetzung dieser Arbeit, semantisches Wissen der
linearen Arithmetik in die Beweisverfahren von AProVE zur partiellen
Korrektheit einzubringen.

Zur Behandlung der linearen Arithmetik führen wir die Problemstellung
häufig auf lineare Optimierungsprobleme zurück. Zu deren Lösung greifen
wir auf das Simplex-Verfahren mit der Gomory-Erweiterung zurück. In
dieser Arbeit werden also Ideen der Informatik, der Mathematik und des
Operations Research in AProVE miteinander kombiniert, und somit wird die
Zielsetzung erreicht.