Induction Proofs for Second-Order Procedures in VeriFun

Zum Inhalt:

Der Vortrag beschreibt eine Erweiterung von VeriFun, die das Führen von (Induktions-)Beweisen über Programme mit Prozeduren zweiter Ordnung (wie z. B. 'map' und 'filter') ermöglicht. Die Erweiterung umfasst insbesondere folgende Aspekte:

- automatische Verwendung von Lemmata mittels Matching

- Behandlung unvollständig definierter Prozeduren (wie etwa die

   Übergabe der Divisionsfunktion an eine Prozedur zweiter Ordnung)

- automatische Widerlegung von Aussagen, die Funktionsvariablen

   enthalten