Unsound Inferences Make Proofs Shorter.
JOURNAL OF SYMBOLIC LOGIC（2019）
摘要
We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter than LK-proofs.
更多查看译文
关键词
unsound inferences,sequent calculus,cut elimination,eigenvariable condition
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要