Weidenbach, Christoph

Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen

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.