CoqHammer
From MaRDI portal
Software:41110
No author found.
Source code repository: https://github.com/lukaszcz/coqhammer
Related Items (18)
Deepalgebra -- an outline of a program ⋮ Proof mining with dependent types ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Aligning concepts across proof assistant libraries ⋮ Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings ⋮ Relaxed weighted path order in theorem proving ⋮ The Coq library as a theory graph ⋮ A plugin to export Coq libraries to XML ⋮ Concrete semantics with Coq and CoqHammer ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ Experiences from exporting major proof assistant libraries
This page was built for software: CoqHammer