Interactive Theorem Proving systems become more important in certifying mathematical proofs and properties of software and hardware. A large part of the process of proof formalization consists of providing justifications for smaller goals. Many of such goals would be considered trivial by mathematicians. Still, modern ITPs require users to spend an important part of the formalization effort on such easy goals. ITP automation techniques are able to reduce this effort significantly. The strongest general purpose proof assistant automation technique is today provided by tools called “hammers” which combine learning from previous proofs with a translation of the problems to the logics of automated systems and reconstruction of the successfully found proofs. In this talk, an overview of the hammer tool for Coq proof assistant will be given.
Czajka, Ł., & Kaliszyk, C. (2018). Hammer for Coq: Automation for dependent type theory. Journal of automated reasoning, 61 (1-4), 423-453.
Presenter --- Eugene Moiseenko
Date: April 22, 2019
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28