A tree rewriting system for the Reflection Calculus
Sof\'ia Santiago-Fern\'andez, Joost J. Joosten, David, Fern\'andez-Duque

TL;DR
This paper introduces a tree rewriting system, ${ m TRC}$, that effectively simulates the Reflection Calculus, enabling improved proof search and formalization in proof assistants, with applications in proof theory and ordinal analysis.
Contribution
The paper presents ${ m TRC}$, a novel tree rewriting system that is complete and adequate for the Reflection Calculus, facilitating proof search and formalization.
Findings
${ m TRC}$ is complete and adequate for $ ext{f RC}$.
Normalization theorem improves proof search efficiency.
Formalization in proof assistants is facilitated.
Abstract
The () is the fragment of the polymodal logic in the language whose formulas are built up from and propositional variables using conjunction and diamond modalities. is complete with respect to the arithmetical interpretation that associates modalities with reflection principles and has various applications in proof theory, specifically ordinal analysis. We present , a tree rewriting system that is adequate and complete with respect to , designed to simulate derivations. is based on a given correspondence between formulas of and modal trees . Modal trees are presented as an inductive type allowing precise positioning and transformations which give rise to the formal definition of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Advanced Database Systems and Queries · Distributed and Parallel Computing Systems
