Hammering towards QED
From MaRDI portal
Publication:5195271
DOI10.6092/ISSN.1972-5787/4593zbMATH Open1451.68318OpenAlexW2262606152MaRDI QIDQ5195271FDOQ5195271
Authors: Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban, Lawrence C. Paulson 
Publication date: 18 September 2019
Full work available at URL: https://hal.inria.fr/hal-01386988
Recommendations
- Advances in QED with intense background fields
- QED coupled to QEG
- On the construction of QED using ERG
- On the way from Sakatons to quarks
- A perspective on external field QED
- On the gauge parameter dependence of QED
- QED in the clothed-particle representation
- scientific article; zbMATH DE number 1944690
- The Compton effect as one path to QED
- Constructing the light-front QCD Hamiltonian
Cited In (40)
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Faster, higher, stronger: E 2.3
- Verifying OpenJDK's sort method for generic collections
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Guiding an automated theorem prover with neural rewriting
- Vampire with a brain is a good ITP hammer
- Lyndon words formalized in Isabelle/HOL
- Finding proofs in Tarskian geometry
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation
- Title not available (Why is that?)
- Targeted configuration of an SMT solver
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Learning theorem proving components
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Formalising basic topology for computational logic in simple type theory
- GRUNGE: a grand unified ATP challenge
- System description: E.T. 0.1
- Hierarchical invention of theorem proving strategies
- Limited second-order functionality in a first-order setting
- HOL(y)Hammer: online ATP service for HOL Light
- A bi-directional extensible interface between Lean and Mathematica
- Solving hard Mizar problems with instantiation and strategy invention
- Conditional normative reasoning as a fragment of HOL
- Extending SMT solvers to higher-order logic
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Practical Proof Search for Coq by Type Inhabitation
- Recurrence-Driven Summations in Automated Deduction
- Automating formalization by statistical and semantic parsing of mathematics
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Machine Learning for Inductive Theorem Proving
- Learning to parse on aligned corpora (rough diamond)
- Theorem proving as constraint solving with coherent logic
- Extending a high-performance prover to higher-order logic
- Machine-learned premise selection for Lean
- Hammer for Coq: automation for dependent type theory
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Uses Software
This page was built for publication: Hammering towards QED
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195271)
