论文标题
引入证明树自动机和证明树图
Introducing Proof Tree Automata and Proof Tree Graphs
论文作者
论文摘要
在结构证明理论中，设计和研究大量微积分使得很难单独和作为整个系统的一部分获得有关每个规则的直觉。我们介绍了两个新颖的工具，以使用图理论和自动机理论的方法来帮助进行微积分。第一个工具是证明树自动机（PTA）：树自动机哪种语言是微积分的派生语言。第二个工具是一个称为证明树图（PTG）的演算的图形表示。在此定向的超图中，顶点是术语（例如序列），而超级弧是规则。我们探索PTA和PTG的属性以及它们之间的关系。我们表明，我们可以将PTA作为从微积分到传统树自动机的部分地图分解。我们在改进系统理论中制定了这一说法。最后，我们将框架与证明网和弦图进行比较。
In structural proof theory, designing and working on large calculi make it difficult to get intuitions about each rule individually and as part of a whole system. We introduce two novel tools to help working on calculi using the approach of graph theory and automata theory. The first tool is a Proof Tree Automaton (PTA): a tree automaton which language is the derivation language of a calculus. The second tool is a graphical representation of a calculus called Proof Tree Graph (PTG). In this directed hypergraph, vertices are sets of terms (e.g. sequents) and hyperarcs are rules. We explore properties of PTA and PTGs and how they relate to each other. We show that we can decompose a PTA as a partial map from a calculus to a traditional tree automaton. We formulate that statement in the theory of refinement systems. Finally, we compare our framework to proof nets and string diagrams.
