__Journal article:__

** Misha Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann
Pitassi.
"Minimum Propositional Proof Length is NP-Hard to Linearly
Approximate."
Journal of Symbolic Logic 66 (2001) 171-191.**

** Download journal article version: postscript
or PDF. **

__Conference proceedings (earlier version).__

**Misha Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann
Pitassi.
"Minimum Propositional Proof Length is NP-Hard to Linearly
Approximate (Extended Abstract)."
Proceedings, Mathematical Foundations of Computer Science (MFCS'98)
Lecture Notes in Computer Science #1450,
Springer-Verlag, 1998, pp. 176-184.**

** Download conference proceedings extended abstract: postscript or PDF.**

** Journal version abstract: **We prove that the problem
of determining the minimum propositional proof length is NP-hard to approximate within a
factor of \factor. 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.