Komplexität aussagenlogischer Beweissysteme und monotoner Schaltkreise, sowie deren Zusammenhang mittels monotoner effektiver Interpolation

• Antragsteller: Dr. Jan Johannsen
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1999 bis 2004
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5209996

Es sollen Probleme aus Komplexitätstheorie monotoner Schaltkreise und ihre Anwendung auf Probleme aus der Theorie der Komplexität aussagenlogischer Beweissysteme untersucht werden. Insbesondere sollen Schranken an die Tiefe und Größe boolescher Schaltkreise verbessert und auf weitere Klassen monotoner Schaltkreise verallgemeinert werden. Als Anwendung folgen neue und verbesserte untere Schranken für aussagenlogische Beweissysteme, etwa Varianten des Cutting-Planes Systems, mittels der Methode der effektiven monotonen Interpolation. Weiterhin soll untersucht werden, inwieweit diese Interpolationsmethode auf verschiedene, in der Literatur vorgeschlagene und neue Erweiterung von Cutting-Planes-Beweissystemen verallgemeinert werden kann. Außerdem soll die relative Komplexität von eingeschränkten Formen des Resolutionskalküls untersucht werden. Dabei sollen insbesondere solche Einschränkungen betrachtet werden, die in Anwendungen, etwa in automatischen Theorembeweisern oder in Erfüllbarkeitsalgorithmen, verwendet werden, beispielsweise negative/positive Resolution, reguläre und Davis-Putnam-Resolution oder lineare Resolution.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen