Skip to content

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

License

Notifications You must be signed in to change notification settings

jnarboux/coqhammer

 
 

Repository files navigation

CoqHammer (dev) for Coq 8.11

Travis

CoqHammer video tutorial: part 1 (sauto), part 2 (hammer).

Since version 1.3, the CoqHammer system consists of two major separate components.

  1. The sauto general proof search tactic for the Calculus of Inductive Construction.

  2. 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.

Requirements

Copyright and license

Copyright (c) 2017-2020, 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.

About

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • OCaml 59.6%
  • Coq 29.8%
  • C++ 7.6%
  • Shell 1.2%
  • Makefile 1.1%
  • C 0.6%
  • Nix 0.1%