Published: 17th June 2016|
|Generic Automation for the Coq Proof Assistant: Design and Principles Pierre Corbineau||1|
|Proof Generation in Propositional Intuitionistic Logic Based upon Automata Theory Aleksy Schubert and Maciej Zielenkiewicz||2|
|Extending Nunchaku to Dependent Type Theory Simon Cruanes and Jasmin Christian Blanchette||3|
|Goal Translation for a Hammer for Coq (Extended Abstract) Łukasz Czajka and Cezary Kaliszyk||13|
|Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds and Cesare Tinelli||21|
|Towards the Integration of an Intuitionistic First-Order Prover into Coq Fabian Kunze||30|
This volume of EPTCS contains the proceedings of the First Workshop on Hammers for Type Theories (HaTT 2016), held on 1 July 2016 as part of the International Joint Conference on Automated Reasoning (IJCAR 2016) in Coimbra, Portugal.
HOLyHammer for HOL Light and HOL4, Sledgehammer for Isabelle/HOL, and other similar tools can have a huge impact on user productivity. These integrate automatic theorem provers (including SMT solvers) with proof assistants. However, users of proof assistants based on type theories, such as Agda, Coq, Lean, and Matita, currently miss out on this convenience. The expressive, constructive logic is often seen as an insurmountable obstacle, but large developments, including the CompCert compiler, typically postulate the classical axioms and use dependent types sparingly.
The workshop features four regular papers, three regular presentations, and two invited talks by Pierre Corbineau (Verimag, France) and Aleksy Schubert (University of Warsaw, Poland).
We would like to thank the authors for submitting papers of high quality to these proceedings, the program committee and external reviewers for diligently reviewing the submissions, and the local organizers of IJCAR 2016 for their help in organizing HaTT 2016.
6 July 2016
Jasmin Christian Blanchette
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.
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.