CoqHammer (dev) for Coq 8.19 (use other branches for other versions of Coq)
CoqHammer video tutorial: part 1 (sauto), part 2 (hammer).
Since version 1.3, the CoqHammer system consists of two major separate components.
The sauto
general proof search tactic for the Calculus of
Inductive Construction.
The hammer
automated reasoning tool which combines learning from
previous proofs with the translation of problems to the logics of
external automated systems and the reconstruction of successfully
found proofs with the sauto
procedure.
See the CoqHammer webpage for documentation and installation instructions.
Copyright (c) 2017-2024, Lukasz Czajka, TU Dortmund University.\ Copyright (c) 2017-2018, Cezary Kaliszyk, University of Innsbruck.
Distributed under the terms of LGPL 2.1, see the file LICENSE.
See CREDITS for a full list of contributors.