swMATH29396MaRDI QIDQ41110FDOQ41110
Author name not available (Why is that?)
Official website: http://cl-informatik.uibk.ac.at/cek/coqhammer/
Source code repository: https://github.com/lukaszcz/coqhammer
Cited In (39)
- 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?)
- Satallax
- ML4PG
- Polar
- JProver
- HOLyHammer
- HOT
- Beagle
- Aligator.jl
- MathTools
- RISCAL
- Lambda Free RPOs
- VerifyThis
- MathChat
- CoqInE
- Logipedia
- SMTCoq
- Zipperposition
- Concrete semantics with Coq and CoqHammer
- SETL
- egg
- Extending SMT solvers to higher-order logic
- Experiences from exporting major proof assistant libraries
- Practical Proof Search for Coq by Type Inhabitation
- Goeland
- EUCLID
- A plugin to export Coq libraries to XML
- The Coq library as a theory graph
This page was built for software: CoqHammer
