JAIST Logic@JAIST

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