de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
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: http://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.