English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Thesis

Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen

MPS-Authors
/persons/resource/persons45719

Weidenbach,  Christoph       
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

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


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-331D-D
Abstract
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.