A sequent calculus with procedure calls
CoRR(2012)
摘要
In this paper, we extend the sequent calculus LKF into a calculus LK(T), allowing calls to a decision procedure. We prove cut-elimination of LK(T).
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要