CoqHammer is a general-purpose automated reasoning hammer tool for Coq. It combines learning from previous proofs with the translation of problems to the logics of automated systems and the reconstruction of successfully found proofs. A typical use is to prove relatively simple goals using available lemmas. The problem is to find appropriate lemmas in a large collection of all accessible lemmas and combine them to prove the goal. The advantage of a hammer is that it is a general system not depending on any domain-specific knowledge and not requiring configuration by the user. The hammer plugin may use all currently accessible lemmas, including those proven earlier in a given formalization, not only the lemmas from predefined libraries or hint databases. At present, however, best results are achieved for statements ”close to” first-order logic and lemmas from the standard library or similar.

References in zbMATH (referenced in 16 articles , 1 standard article )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  2. Czajka, Łukasz: A new coinductive confluence proof for infinitary lambda calculus (2020)
  3. Jakubův, Jan; Kaliszyk, Cezary: Relaxed weighted path order in theorem proving (2020)
  4. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  5. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  6. Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
  7. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  8. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  9. Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
  10. Sacerdoti Coen, Claudio: A plugin to export Coq libraries to XML (2019)
  11. Czajka, Łukasz; Ekici, Burak; Kaliszyk, Cezary: Concrete semantics with Coq and CoqHammer (2018)
  12. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  13. Rabe, Florian (ed.); Farmer, William M. (ed.); Passmore, Grant O. (ed.); Youssef, Abdou (ed.): Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (2018)
  14. Chojecki, Przemysław: Deepalgebra -- an outline of a program (2017)
  15. Czajka, Łukasz: Confluence of an extension of combinatory logic by Boolean constants (2017)
  16. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)