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

✍ Scribed by Noriko H. Arai

• Publisher: Elsevier Science
• Year: 2000
• Tongue: English
• Weight: 106 KB
• Volume: 104
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(00)00005-1

✦ Synopsis

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 e ciency 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 e ciency. 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.