Guiding an automated theorem prover with neural rewriting

DOI10.1007/978-3-031-10769-6_35OpenAlexW4289104042MaRDI QIDQ2104548

Jelle Piepenbrock, Tom Heskes, Mikoláš Janota, Josef Urban

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_35

zbMATH Keywords

machine learningautomated theorem provingabelian inner mapping

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Loops, quasigroups (20N05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• z3
• Prover9
• HOL
• E Theorem Prover
• Waldmeister
• PyTorch
• Adam
• GitHub
• Twee
• ENIGMA
• HOList
• ACER

Cites Work

• Unnamed Item
• Unnamed Item
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• TacticToe: learning to prove with tactics
• Twee: an equational theorem prover
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• Tree neural networks in HOL4
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Faster, higher, stronger: E 2.3
• Premise selection for mathematics by corpus analysis and kernel methods
• Automated theorem proving in quasigroup and loop theory
• A New Class of Automated Theorem-Proving Algorithms
• Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
• Citius altius fortius
• The CADE-27 Automated theorem proving System Competition – CASC-27
• Hammering towards QED
• Proof simplification and automated theorem proving
• ACER

This page was built for publication: Guiding an automated theorem prover with neural rewriting