Introducing Proof Tree Automata and Proof Tree Graphs

TL;DR

This paper introduces two innovative graph-theoretic tools, Proof Tree Automata and Proof Tree Graphs, to improve understanding and analysis of large calculi in structural proof theory.

Contribution

The paper presents novel automata and graphical representations for calculi, enabling better intuition and analysis through graph and automata theory.

Findings

Proof Tree Automata can represent derivation languages of calculi.

Proof Tree Graphs provide a hypergraph visualization of calculi rules.

Framework relates automata and graphs to proof nets and string diagrams.

Abstract

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.