Journal of Symbolic Logic 66 (1):171-191 (2001)
AbstractWe prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.
Similar books and articles
Quantified propositional logic and the number of lines of tree-like proofs.Alessandra Carbone - 2000 - Studia Logica 64 (3):315-321.
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Propositional proof systems, the consistency of first order theories and the complexity of computations.Jan Krajíček & Pavel Pudlák - 1989 - Journal of Symbolic Logic 54 (3):1063-1079.
Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Proving theorems of the second order Lambek calculus in polynomial time.Erik Aarts - 1994 - Studia Logica 53 (3):373 - 387.
Bounded Arithmetic, Propositional Logic and Complexity Theory.Jan Krajíček - 1995 - Cambridge University Press.
Polynomial size proofs of the propositional pigeonhole principle.Samuel R. Buss - 1987 - Journal of Symbolic Logic 52 (4):916-927.
Review: Michael Alekhnovich, Sam Buss, Shlomo Moran, Toniann Pitassi, Minimum Propositional Proof Length Is NP-Hard to Linearly Approximate. [REVIEW]Alexander Razborov - 2002 - Bulletin of Symbolic Logic 8 (2):301-302.
Added to PP
Historical graph of downloads