Detailseite
Projekt Druckansicht

Vollautomatisches Beweisen in modaler Prädikatenlogik: Kalküle, Implementierungen und Problemsammlungen

Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2009 bis 2014
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 129761239
 
Beweisführung in modaler Prädikatenlogik hat vielfältige Anwendungen, wie zum Beispiel beim Planen, der Verarbeitung natürlicher Sprache, oder beim Entwurf und der Verifikation sicherheitskritischer Software. Die Effizienz existierender automatischer Beweissysteme reicht jedoch nicht aus, um eine hinreichende Computerunterstützung für derartige Anwendungen zu bieten. Ziel dieses Projektes ist es, die Effizienz von vollautomatischen Beweissystemen für modale Prädikatenlogik signifikant zu steigern. Hierzu sollen verschiedene Kalküle und Beweisverfahren für modale Prädikatenlogik entwickelt werden. Darauf aufbauend werden mehrere leistungsfähige vollautomatische Beweiser implementiert und optimiert. Um einen Vergleich verschiedener Beweissysteme zu ermöglichen und den Fortschritt auf dem Gebiet zu fördern und zu messen, soll, ähnlich zu existierenden Sammlungen für klassische und intuitionistische Logik, eine umfangreiche, standardisierte Sammlung von Problemen für modale Prädikatenlogik sowie eine Testumgebung für entsprechende Beweisverfahren entwickelt und im Internet öffentlich zugänglich gemacht werden.
DFG-Verfahren Sachbeihilfen
 
 

Zusatzinformationen

Textvergrößerung und Kontrastanpassung