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