Cited in
(39)- Relaxed weighted path order in theorem proving
- Aligning concepts across proof assistant libraries
- Practical Proof Search for Coq by Type Inhabitation
- Deepalgebra -- an outline of a program
- Proof mining with dependent types
- Extending SMT solvers to higher-order logic
- scientific article; zbMATH DE number 7204433 (Why is no real title available?)
- Portfolio theorem proving and prover runtime prediction for geometry
- Satallax
- ML4PG
- Polar
- JProver
- HOLyHammer
- HOT
- Beagle
- Aligator.jl
- MathTools
- RISCAL
- Lambda Free RPOs
- VerifyThis
- MathChat
- CoqInE
- Logipedia
- SMTCoq
- Zipperposition
- SETL
- egg
- scientific article; zbMATH DE number 7199590 (Why is no real title available?)
- Making higher-order superposition work
- Superposition with lambdas
- A plugin to export Coq libraries to XML
- The Coq library as a theory graph
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings
- Concrete semantics with Coq and CoqHammer
- Superposition with lambdas
- Goeland
- EUCLID
- Experiences from exporting major proof assistant libraries
- Restricted combinatory unification
This page was built for software: CoqHammer
