Abstract

Hammers are tools that provide general purpose automation for
formal proof assistants. Despite the gaining popularity of the more
advanced versions of type theory, there are no hammers for such
systems. We present an extension of the various hammer components to
type theory: (i) a translation of a significant part of the Coq logic
into the format of automated proof systems; (ii) a proof
reconstruction mechanism based on a Ben-Yelles-type algorithm combined
with limited rewriting, congruence closure and a first-order
generalization of the left rules of Dyckhoff’s system LJT.

BibTeX

@inproceedings{lcck-hatt16,
 author    = {\L{}ukasz Czajka and
              Cezary Kaliszyk},
 title     = {Goal Translation for a Hammer for Coq (Extended Abstract)},
 booktitle = {Proceedings First International Workshop on Hammers for
Type Theories (HaTT 2016)},
 pages     = {13--20},
 year      = {2016},
 doi       = {10.4204/EPTCS.210.4},
 editor    = {Jasmin Blanchette and
              Cezary Kaliszyk},
 series    = {{EPTCS}},
 volume    = {210},
}