Guiding an automated theorem prover with neural rewriting

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

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

Recommendations

• scientific article; zbMATH DE number 1748489
• A neurally-guided, parallel theorem prover
• Deep network guided proof search
• Automated proof synthesis for the minimal propositional logic with deep neural networks
• Toward neural-network-guided program synthesis and verification
• A fully automatic theorem prover with human-style output
• The term rewriting approach to automated theorem proving
• Verifying B proof rules using deep embedding and automated theorem proving

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)

Cites Work

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

Cited In (2)

• An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)
• Automated proof synthesis for the minimal propositional logic with deep neural networks

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104548)