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