Cut-free LK quasi-polynomially simulates resolution
Logic
2009-09-25 v1
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.
Cite
@article{arxiv.math/9804159,
title = {Cut-free LK quasi-polynomially simulates resolution},
author = {Noriko Arai},
journal= {arXiv preprint arXiv:math/9804159},
year = {2009}
}