Aguilera Ozuna, J. P., & Baaz, M. (2019). Unsound Inferences Make Proofs Shorter. Journal of Symbolic Logic, 84(1), 102–122. https://doi.org/10.1017/jsl.2018.51
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 nonelementarily shorter than LK-proofs.
en
Research Areas:
außerhalb der gesamtuniversitären Forschungsschwerpunkte: 100%