Introducing Proof Tree Automata and Proof Tree Graphs
This work addresses a niche problem for researchers in structural proof theory by providing incremental tools to improve intuition and analysis of calculi.
The paper tackles the difficulty of understanding and working with large calculi in structural proof theory by introducing Proof Tree Automata (PTA) and Proof Tree Graphs (PTG) as tools based on graph and automata theory, exploring their properties and relationships, and comparing them to existing frameworks like proof nets and string diagrams.
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.