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