Note on Globally Sound Analytic Calculi for Quantifier Macros.
WoLLIC(2019)
摘要
This paper focuses on a globally sound but possibly locally unsound analytic sequent calculus for the quantifier macro Q defined by Q(x,y)A(x, y) = for all x there exists yA(x, y). It is demonstrated that no locally sound analytic representation exists.
更多查看译文
关键词
Sequent calculus, Cut-elimination, Quantifier macros
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络