Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematical structure. For this to be possible, proof systems must be designed as a set of rules such that proofs using those rules are correct by construction. Therefore, one must consider all ways these rules can interact and prove that they satisfy certain properties which makes them "well-behaved". This is called the meta-theory of a proof system. Meta-theory proofs typically involve many cases on structures with lots of symbols. The majority of cases are usually quite similar, and when a proof fails, it might be because of a sub-case on a very specific configuration of rules. Developing these proofs by hand is tedious and error-prone, and their combinatorial nature suggests they could be automated. There are various approaches on how to automate, either partially or completely, meta-theory proofs. In this paper, I will present some techniques that I have been involved in for facilitating meta-theory reasoning.
翻译:结构性证据理论被称赞为一种对推理和证据的象征性方法,在这种方法中,人们可以界定推理步骤的模型,并将证据作为数学结构来操纵证据。要做到这一点,就必须将证据系统设计成一套规则,使使用这些规则的证明能够通过构建来正确。因此,我们必须考虑所有这些规则能够相互作用并证明它们满足某些特性,从而使其“以良好方式执行”的各种方式。这被称为一个证明系统的元理论。元理论证据通常涉及许多带有许多符号的结构上的许多案例。多数案例通常非常相似,当证据失败时,这可能是由于规则的非常具体配置的子案例。用手来开发这些证据是乏味和易出错的,其组合性质表明它们可以自动化。对于如何将部分或完全的元理论证据自动化,有多种方法。在本文中,我将介绍一些我参与其中的技巧,以促进元理论推理。