complexity of prospositional proof systems and monotone circuits

• Applicant: Dr. Jan Johannsen
• Subject Area: Theoretical Computer Science
• Term: from 1999 to 2004
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Independent Junior Research Groups