Erlernen der Techniken automatischer Beweistransformation, Erlernen der semi-automatischen Analyse mathematischer Beweise.
Das System CERES zur automatischen Schnittelimination mittels Resolution. Erweiterung von CERES durch hoehere Ein- und Ausgabesprachen, Experimente mit Schnitt-Elimination in mathematischen Beweisen. Teilnehmer muessen an den woechentlichen Treffen der CERES-Projektgruppe teilnehmen.
Details zur Lehrveranstaltung auf www.logic.at/lvas/185302
Der erfolgreiche Abschluss der Lehrveranstaltung erfordert: (1) Programmentwicklung, (2) Dokumentation der Arbeit in einem Bericht (ca 10 Seiten), (3) Praesentation der Resultate bei einer CERES-Projektbesprechung.
Nicht erforderlich