Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):
M. Baaz, J. Aguilera Ozuna:
"Unsound Inferences make proofs shorter";
Vortrag: CS Theory Seminar,
Calgary (eingeladen);
03.03.2017.
Kurzfassung englisch:
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.
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.