Talks and Poster Presentations (without Proceedings-Entry):
M. Baaz, J. Aguilera Ozuna:
"Unsound Inferences make proofs shorter";
Talk: CS Theory Seminar,
Calgary (invited);
2017-03-03.
English abstract:
We give examples of analytic sequent calculi that extend Gentzenīs sequent calculus LK by unsound quantifier rules in such a way that (i) derivations lead only to true sequents and (ii) cut free proofs may be non-elementary shorter than cut free LK proofs.
This Research is based on properties of Hilbertīs Epsilon calculus and part of efforts to complement Hilbertīs stepwise concept of proof by useful global concepts.
Created from the Publication Database of the Vienna University of Technology.