On the Automatizability of Resolution and Related Propositional Proof Systems

A propositional proof system is automatizable if there is an algorithm that, given a tautology, produces a proof in time polynomial in the size of its smallest proof. This notion can be weakened if we allow the algorithm to produce a proof in a stronger system within the same time bound. This new notion is called weak automatizability. Among other characterizations, we prove that a system is weakly automatizable exactly when a weak form of the satisfiability problem is solvable in polynomial time. After studying the robustness of the definition, we prove the equivalence between: (i) Resolution is weakly automatizable, (ii) Res(

• Type: Journal
• Year: 2002
• Where: CSL
• Authors: Albert Atserias, Maria Luisa Bonet
• Keywords: Automated Reasoning, CSL 2002, Polynomial, Propositional Proof, Smallest Proof