Affordable Access

Publisher Website

Relative efficiency of propositional proof systems: resolution vs. cut-free LK

Authors
Journal
Annals of Pure and Applied Logic
0168-0072
Publisher
Elsevier
Publication Date
Volume
104
Identifiers
DOI: 10.1016/s0168-0072(00)00005-1
Keywords
  • Cut-Elimination
  • Proof Complexity
  • Resolution
Disciplines
  • Computer Science

Abstract

Abstract Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 (Reckhow, Ph.D. Thesis, University of Toronto, 1976; A. Urquhart, the complexity of propositional proofs, Bull. of Symbolic Logic 1 (1995) 425–467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 (1979) 36–50 that tree resolution has super-polynomial speed-up over (tree) cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as directed acyclic graphs (DAG) have the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK (DAG) polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK (DAG). We also show that cut-free LK (DAG) polynomially simulates regular resolution.

There are no comments yet on this publication. Be the first to share your thoughts.