Hammering towards QED
From MaRDI portal
Publication:5195271
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
- Guiding an automated theorem prover with neural rewriting
- Vampire with a brain is a good ITP hammer
- Lyndon words formalized in Isabelle/HOL
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Finding proofs in Tarskian geometry
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- 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
- GRUNGE: a grand unified ATP challenge
- Formalising basic topology for computational logic in simple type theory
- 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
- Automating formalization by statistical and semantic parsing of mathematics
- Practical Proof Search for Coq by Type Inhabitation
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Recurrence-Driven Summations in Automated Deduction
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Learning to parse on aligned corpora (rough diamond)
- Machine Learning for Inductive Theorem Proving
- Theorem proving as constraint solving with coherent logic
- Hammer for Coq: automation for dependent type theory
- Extending a high-performance prover to higher-order logic
- Machine-learned premise selection for Lean
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Describes a project that uses
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)
