Facilitating Meta-Theory Reasoning (Invited Paper)

Giselle Reis
(Carnegie Mellon University)

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.

In Elaine Pimentel and Enrico Tassi: Proceedings Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2021), Pittsburgh, USA, 16th July 2021, Electronic Proceedings in Theoretical Computer Science 337, pp. 1–12.
Published: 16th July 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.337.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org