{"repo":"lukaszcz/coqhammer","free":true,"listed":false,"github":"https://github.com/lukaszcz/coqhammer","clone":"git clone https://github.com/lukaszcz/coqhammer.git","description":"CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory","language":"OCaml","stars":244,"topics":["coq","hammer","automation","proof-search","theorem-prover","verification","dependent-types","rocq","rocq-prover"],"license":null,"category":"workflow-automation","readme_excerpt":"CoqHammer (dev) for Rocq 9.2 (use other branches for other versions of Rocq) [![Docker CI][docker-action-shield]][docker-action-link] [docker-action-shield]: https://github.com/lukaszcz/coqhammer/actions/workflows/docker-action.yml/badge.svg?branch=rocq-9.2 [docker-action-link]: https://github.com/lukaszcz/coqhammer/actions?query=workflow:\"Docker%20CI\" 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 ------------ - Rocq 9.2 - for hammer : automated provers (Vampire, CVC4, Eprover, and/or Z3) Copyright and license --------------------- Copyright (c) 2017-2026, Lukasz Czajka.\\ 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.","default_branch":null,"files":null,"tree":[],"storefront":"/r/lukaszcz","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/lukaszcz/coqhammer/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}