Complexity of resolution proofs and function introduction

Annals of Pure and Applied Logic 57 (3):181-215 (1992)
  Copy   BIBTEX


The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f are new function symbols extending Herbrand's universe. P ()Q from Q) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions . Finally it is proved that FR-deduction has weaker effects only if clausal logic is restricted to Horn logic



    Upload a copy of this work     Papers currently archived: 91,164

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.
A note on propositional proof complexity of some Ramsey-type statements.Jan Krajíček - 2011 - Archive for Mathematical Logic 50 (1-2):245-255.
The Complexity of Analytic Tableaux.Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart - 2006 - Journal of Symbolic Logic 71 (3):777 - 790.
Pool resolution is NP-hard to recognize.Samuel R. Buss - 2009 - Archive for Mathematical Logic 48 (8):793-798.
Cut normal forms and proof complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
The Complexity of Resolution Refinements.Joshua Buresh-Oppenheim & Toniann Pitassi - 2007 - Journal of Symbolic Logic 72 (4):1336 - 1352.


Added to PP

19 (#750,145)

6 months
4 (#678,769)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
A Resolution Calculus For Shortening Proofs.Nicolas Peltier - 2005 - Logic Journal of the IGPL 13 (3):307-333.

Add more citations

References found in this work

A Machine-Oriented Logic based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.
A Computing Procedure for Quantification Theory.Martin Davis & Hilary Putnam - 1966 - Journal of Symbolic Logic 31 (1):125-126.
On Different Concepts of Resolution.Alexander Leitsch - 1989 - Mathematical Logic Quarterly 35 (1):71-77.
On Different Concepts of Resolution.Alexander Leitsch - 1989 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 35 (1):71-77.

Add more references