Sciweavers

SIAMCOMP
2000
76views more  SIAMCOMP 2000»
13 years 4 months ago
On Interpolation and Automatization for Frege Systems
The interpolation method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system ...
Maria Luisa Bonet, Toniann Pitassi, Ran Raz
FOCS
1999
IEEE
13 years 8 months ago
A Study of Proof Search Algorithms for Resolution and Polynomial Calculus
This paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof systems: Resolution and Polynomial Calculus (PC). For the former syste...
Maria Luisa Bonet, Nicola Galesi
ICALP
2007
Springer
13 years 10 months ago
Complexity of Propositional Proofs Under a Promise
Abstract. We study – within the framework of propositional proof complexity – the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiabl...
Nachum Dershowitz, Iddo Tzameret
SAT
2009
Springer
153views Hardware» more  SAT 2009»
13 years 11 months ago
Does Advice Help to Prove Propositional Tautologies?
One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [6], where they defined propositional proof systems as poly-time computable f...
Olaf Beyersdorff, Sebastian Müller
LATA
2009
Springer
13 years 11 months ago
Nondeterministic Instance Complexity and Proof Systems with Advice
Abstract. Motivated by strong Karp-Lipton collapse results in bounded arithmetic, Cook and Kraj´ıˇcek [7] have recently introduced the notion of propositional proof systems with...
Olaf Beyersdorff, Johannes Köbler, Sebastian ...