Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen

Weidenbach, Christoph

Datensatz

DATENSATZ AKTIONENEXPORT

DownloadE-Mail

Bitte beachten Sie, dass eine neuere Version dieses Datensatzes verfügbar ist:
https://pure.mpg.de/pubman/item/item_1330773_3

DetailsÜbersicht

Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen

Weidenbach, C. (2000). Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen. Habilitation Thesis, Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät, Saarbrücken.

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-331D-D Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-ACD3-4

Genre: Hochschulschrift

ausblenden:

Urheber:
Weidenbach, Christoph^{1, 2}, Autor

Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

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.