Datensatz

Zusammenfassung

Abstract der Antrittsvorlesung: Heute lassen sich mit modernen Beweissystemen fuer die klassische Praedikatenlogik eine Reihe von aktuellen Problemen wie die Analyse von Programmen oder (Sicherheits)Protokollen vollautomatisch loesen. Dies ist das Resultat einer Reihe von neuen Techniken/Ergebnissen, die in Form von Kalkuelen, Redundanzkriterien, Algorithmen und Implementierungsdesigns Einzug in aktuelle Systeme gehalten haben. In der Vorlesung werde ich, ausgehend von der Eingabe des Beweissystems, einer Formel, bis hin zu seinem Resultat bei Terminierung, dem Beweis oder der saturierten und damit erfuellbaren Klauselmenge, die in dem SPASS-Beweissystem realisierten Techniken vorstellen und sie aus theoretischer, pragmatischer und Implementierungssicht diskutieren und demonstrieren.