Unsound inferences make proofs shorter
Matthias BaazVienna University of Technology
2016/12/06 (Tue) 15:20
JAIST, Collaboration room 6 (I-57)
Abstract: We give examples of calculi that extend Gentzen's sequent calculus LK in such a way that (i) derivations lead only to true sequents (ii) cut free proofs may be non-elementary shorter than cut free LK proofs.