arXiv · math/9804159
Cut-free LK quasi-polynomially simulates resolution
Abstract
In this paper, the relative efficiency of two propositional systems is studied: resolution and cut-free LK in DAG. We give an upper bound for translation of resolution refutation to cut-free LK proofs. The best upper bound known was 2.
Explore related subjects
Keep this discovery
Noriko Arai. 1998-04-01. Cut-free LK quasi-polynomially simulates resolution. https://arxiv.org/abs/math/9804159
Cite the original work for its findings. Save a collection to share your selection of sources.