Olga Tveretina
Relative Efficiency of Propositional Proof Systems Based on Resolution and OBDDs
The Knowledge Based Systems Group hosted a joint talk with Olga Tveretina
| DATE: | Monday, February 13, 2012 |
| TIME: | 11:00 – 12:00 |
| VENUE: | Seminarroom Goedel (Favoritenstrasse 9-11, ground floor, access through courtyard) |
ABSTRACT
One of the most important questions in proof complexity is: Given a universally valid statement, what is the length of the shortest proof in some standard proof system? This question has a fundamental implication for complexity theory: There exists a propositional proof systems producing polynomial size proofs for all tautologies if and only if NP equals co-NP.
Therefore, studying standard proof systems is interesting due to the following reasons: 1) Theorem-proving systems implement a procedure based on a standard proof systems, and 2) lower bounds on standard proof systems show that a certain class of algorithms needs exponential time in the worst case.
Olga Tveretina presented some lower bounds and compare the relative efficiency of proof systems based on resolution and Ordered Binary Decision Diagrams.
With kind support of the Vienna Center for Logic and Algorithms (VCLA), the Center for Computer Science (CCS) and the Wolfgang Pauli Institut (WPI).
