Proof Generation in Propositional Intuitionistic Logic Based upon Automata Theory

The process of proof construction in constructive logics corresponds very naturally to runs of a certain kind of automata. This idea was used as a presentation method in recent book on lambda calculi with types by Barendregt, Dekkers, and Statman. However, this idea also gives the opportunity to bring the refined techniques of automata theory to proof generation in constructive logics. In the talk a model of automata will be presented that can handle proof construction in full intuitionistic first-order logic. The automata are constructed in such a way that any successful run corresponds directly to a cut-free proof in the logic. This makes it possible to discuss formal languages of proofs and the closure properties of the automata and their connections with the traditional logical connectives. It turns out that one can devise two natural notions of automata. The first one that is able to recognise the language of all the normal forms and one that is able to recognise only proofs in so called total discharge form. This difference will be discussed during the talk as well as a number of decision problems around the automata. Of course, the emptiness problem for automata in their most general presentation is undecidable, but a number of interesting decidable cases will be presented during the talk. The languages of proofs discussed so far are languages of cut-free proofs. However, proofs in proof assistants are usually constructed with help of lemmas and the cut rule is used there extensively. An automata theoretic approach to proofs with cuts will also be discussed during the talk.