Formalized Meta-Theory of Sequent Calculi for Substructural Logics.
Electronic Notes in Theoretical Computer Science(2017)
摘要
When studying sequent calculi, proof theorists often have to prove properties about the systems, whether it is to show that they are “well-behaved”, amenable to automated proof search, complete with respect to another system, consistent, among other reasons. These proofs usually involve many very similar cases, which leads to authors rarely writing them in full detail, only pointing to one or two more complicated cases. Moreover, the amount of details makes them more error-prone for humans. Computers, on the other hand, are very good at handling details and repetitiveness.
更多查看译文
关键词
Sequent calculus,cut-elimination,formalized proof,linear logic,Abella
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络