Unsound Inferences Make Proofs Shorter
Logic
2019-05-07 v2 Logic in Computer Science
Abstract
We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs.
Cite
@article{arxiv.1608.07703,
title = {Unsound Inferences Make Proofs Shorter},
author = {Juan P. Aguilera and Matthias Baaz},
journal= {arXiv preprint arXiv:1608.07703},
year = {2019}
}
Comments
21 pages. July 2017 preprint