Pierre Corbineau: Generic automation for the Coq proof assistant: Design and principles
Proof-editing in the Coq proof assistant is conducted using a wide variety of procedures called tactics. Several of these tactics host automated proof-search procedures addressing generic or specific logical problems.
Generic automation tactics try to provide help without relying on the existence of a specific theory or axiom, whereas specialised tactics address logical problems expressed in specific object-level theories such as linear arithmetic, rings, fields…
In this talk, we will focus on several examples of generic automation procedures. We will first describe how they work, and then show how they can interact with each other and other Coq features. Finally we will discuss their usefulness and weaknesses, and the pertinence of the generic approach.
Aleksy Schubert: Proof Generation in Propositional Intuitionistic Logic Based upon Automata Theory
(joint work with Maciej Zielenkiewicz)
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.
