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

• Antragsteller: Professor Dr. Christoph Kreitz
• 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