反射演算的树重写系统
A tree rewriting system for the Reflection Calculus
AI总结：
本文提出一个针对反射演算的树重写系统，用于模拟其推导，并通过规范化提高证明搜索效率，以辅助研究该逻辑的子公式性质和规则可容许性。
摘要：
反射演算（$\mathcal{\mathbf{RC}}$）是语言 $L^+$ 中多模态逻辑 $\mathcal{\mathbf{GLP}}$ 的一个片段，其公式由 $\top$ 和命题变量通过合取和菱形模态构建。$\mathcal{\mathbf{RC}}$ 相对于将模态与反射原理相关联的算术解释是完备的，并在证明论中，特别是序数分析中，有多种应用。我们提出了 ${\sf TRC}$，一个相对于 $\mathcal{\mathbf{RC}}$ 适当且完备的树重写系统，旨在模拟 $\mathcal{\mathbf{RC}}$ 的推导。${\sf TRC}$ 基于 $L^{+}$ 公式与模态树 ${\sf Tree}^{\Diamond}$ 之间的给定对应关系。模态树被呈现为归纳类型，允许精确定位和变换，从而产生重写规则的形式定义，并便于在证明助手中进行形式化。此外，我们提供了系统规则应用的改写规范化定理。改写过程的规范化提高了证明搜索效率并便于实现。通过提供 ${\sf TRC}$ 作为 $\mathcal{\mathbf{RC}}$ 的高效可证明性工具，我们旨在帮助研究该逻辑的各个方面，如子公式性质和规则可容许性。
英文摘要：
The $Reflection$ $Calculus$ ($\mathcal{\mathbf{RC}}$) is the fragment of the polymodal logic $\mathcal{\mathbf{GLP}}$ in the language $L^+$ whose formulas are built up from $\top$ and propositional variables using conjunction and diamond modalities. $\mathcal{\mathbf{RC}}$ 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 ${\sf TRC}$, a tree rewriting system that is adequate and complete with respect to $\mathcal{\mathbf{RC}}$, designed to simulate $\mathcal{\mathbf{RC}}$ derivations. ${\sf TRC}$ is based on a given correspondence between formulas of $L^{+}$ and modal trees ${\sf Tree}^{\Diamond}$. Modal trees are presented as an inductive type allowing precise positioning and transformations which give rise to the formal definition of rewriting rules and facilitates formalization in proof assistants. Furthermore, we provide a rewrite normalization theorem for systematic rule application. The normalization of the rewriting process enhances proof search efficiency and facilitates implementation. By providing ${\sf TRC}$ as an efficient provability tool for $\mathcal{\mathbf{RC}}$, we aim to help on the study of various aspects of the logic such as the subformula property and rule admissibility.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
