A neurally-guided, parallel theorem prover

DOI10.1007/978-3-030-29007-8_3zbMath1435.68374OpenAlexW2963560424MaRDI QIDQ2180215

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

tableauxATPMCTSgraph convolutional network

Mathematics Subject Classification ID

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

Related Items (1)

\textsf{lazyCoP}: lazy paramodulation meets neurally guided search

Uses Software

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

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