A neurally-guided, parallel theorem prover

DOI10.1007/978-3-030-29007-8_3MaRDI QIDQ2180215zbMATH OpenOpenAlexFDO

Authors Michael Rawson, Giles Reger

Publication date 13 May 2020

Full work available at URL https://www.research.manchester.ac.uk/portal/en/publications/a-neurallyguided-parallel-theorem-prover(d64986e4-5d48-4f6b-9f7c-a329ddd4c6e8).html

zbMATH Keywords

ATPgraph convolutional networkMCTStableaux

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Deep network guided proof search
• Guiding an automated theorem prover with neural rewriting
• scientific article; zbMATH DE number 1809862
• Automatic acquisition of search guiding heuristics
• Development of neural networks for accelerating automated theorem proving: Results for the group theory

Cited in

(10)

• Development of neural networks for accelerating automated theorem proving: Results for the group theory
• Neural precedence recommender
• Guiding an automated theorem prover with neural rewriting
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• scientific article; zbMATH DE number 1728727 (Why is no real title available?)
• Deep network guided proof search
• Automated proof synthesis for the minimal propositional logic with deep neural networks
• Solving hard Mizar problems with instantiation and strategy invention
• Invariant neural architecture for learning term synthesis in instantiation proving
• Machine learning for quantifier selection in cvc5

Describes a project that uses

Uses Software

• VAMPIRE
• Mizar
• MaSh
• E Theorem Prover
• z3
• MaLARea
• FEMaLeCoP
• MPTP
• iProver
• E-MaLeS
• PyTorch
• nanoCoP
• DeepMath
• ENIGMA
• CVC4

This page was built for publication: A neurally-guided, parallel theorem prover

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