Guiding an automated theorem prover with neural rewriting
From MaRDI portal
Publication:2104548
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
Cites work
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- A New Class of Automated Theorem-Proving Algorithms
- ACER
- Automated theorem proving in quasigroup and loop theory
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Faster, higher, stronger: E 2.3
- Hammering towards QED
- Loops with abelian inner mapping groups: an application of automated deduction
- Premise selection for mathematics by corpus analysis and kernel methods
- Proof simplification and automated theorem proving
- Reinforcement learning. An introduction
- TacticToe: learning to prove with tactics
- The CADE-27 automated theorem proving system competition -- CASC-27
- The Tactician. A seamless, interactive tactic learner and prover for Coq
- Tree neural networks in HOL4
- Twee: an equational theorem prover
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
Cited in
(8)- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- A neurally-guided, parallel theorem prover
- Deep network guided proof search
- Property invariant embedding for automated reasoning
- An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)
- Invariant neural architecture for learning term synthesis in instantiation proving
- Automated proof synthesis for the minimal propositional logic with deep neural networks
- Enhancing ENIGMA given clause guidance
Describes a project that uses
Uses Software
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)