The following pages link to Hammering towards QED (Q5195271):
Displaying 22 items.
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- Lyndon words formalized in Isabelle/HOL (Q832940) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
- Verifying OpenJDK's sort method for generic collections (Q1725846) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Guiding an automated theorem prover with neural rewriting (Q2104548) (← links)
- Learning theorem proving components (Q2142080) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Faster, higher, stronger: E 2.3 (Q2305435) (← links)
- Finding proofs in Tarskian geometry (Q2362499) (← links)
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (Q2407885) (← links)
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Learning to Parse on Aligned Corpora (Rough Diamond) (Q2945635) (← links)
- Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448) (← links)
