Hammering towards QED
From MaRDI portal
Publication:5195271
DOI10.6092/issn.1972-5787/4593zbMath1451.68318OpenAlexW2262606152MaRDI QIDQ5195271
Jasmin Christian Blanchette, Josef Urban, Cezary Kaliszyk, Lawrence Charles Paulson
Publication date: 18 September 2019
Full work available at URL: https://hal.inria.fr/hal-01386988
Related Items
Finding proofs in Tarskian geometry, Vampire with a brain is a good ITP hammer, Lyndon words formalized in Isabelle/HOL, Practical Proof Search for Coq by Type Inhabitation, ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Learning theorem proving components, System Description: E.T. 0.1, The role of the Mizar mathematical library for interactive proof development in Mizar, Hammer for Coq: automation for dependent type theory, Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started, Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation, Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL, Learning to Parse on Aligned Corpora (Rough Diamond), A bi-directional extensible interface between Lean and Mathematica, Unnamed Item, Automating formalization by statistical and semantic parsing of mathematics, Machine Learning for Inductive Theorem Proving, Formalising basic topology for computational logic in simple type theory, Targeted configuration of an SMT solver, Verifying OpenJDK's sort method for generic collections, Hierarchical invention of theorem proving strategies, Hammering Mizar by Learning Clause Guidance (Short Paper)., Formalization of the fundamental group in untyped set theory using auto2, TacticToe: learning to prove with tactics, Machine learning guidance for connection tableaux, Formalizing Bachmair and Ganzinger's ordered resolution prover, Limited second-order functionality in a first-order setting, Extending SMT solvers to higher-order logic, GRUNGE: a grand unified ATP challenge, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), Faster, higher, stronger: E 2.3, Theorem proving as constraint solving with coherent logic, Guiding an automated theorem prover with neural rewriting, The 10th IJCAR automated theorem proving system competition – CASC-J10
Uses Software
