Unsound Inferences Make Proofs Shorter

Juan P. Aguilera
Juan P. Aguilera

J. Symb. Log., Volume abs/1608.07703, 2019.

Cited by: 12|Bibtex|Views11|Links
EI

Abstract:

We give examples of calculi that extend Gentzenu0027s sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs.

Code:

Data:

Your rating :
0

 

Tags
Comments