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