Proving Structural Properties Of Sequent Systems In Rewriting Logic
REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2018(2018)
摘要
General and effective methods are required for providing good automation strategies to prove properties of sequent systems. Structural properties such as admissibility, invertibility, and permutability of rules are crucial in proof theory, and they can be used for proving other key properties such as cut-elimination. However, finding proofs for these properties requires inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. This paper aims at developing automatic techniques for proving structural properties of sequent systems. The proposed techniques are presented in the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in Maude and achieve a great degree of automation when used on several sequent systems, including intuitionistic and classical logics, linear logic, and normal modal logics.
更多查看译文
关键词
Rewriting Logic, Sequencing System, Normal Modal Logic, Reflective Implementation, Proof Obligations
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络