Unsound inferences make proofs shorter

Unsound inferences make proofs shorter

Matthias Baaz
Vienna University of Technology
Date: 
2016/12/06 (Tue) 15:20
Place: 
JAIST, Collaboration room 6 (I-57)
Group: 
Logic Unit
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.
Contact
Ishihara Hajime