Neural precedence recommender

DOI10.1007/978-3-030-79876-5_30MaRDI QIDQ2055885zbMATH OpenOpenAlexFDO

Authors Filip Bártek, Martin Suda

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_30

zbMATH Keywords

machine learningsimplification orderinggraph convolutional networksaturation-based theorem provingsymbol precedence

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Machine learning for first-order theorem proving
• A neurally-guided, parallel theorem prover
• CoProver: a recommender system for proof construction
• Learning search control-knowledge for equational deduction

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• AVATAR: The Architecture for First-Order Theorem Provers
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Automated Deduction – CADE-20
• Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Computing small clause normal forms
• Deep learning
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Faster, higher, stronger: E 2.3
• Finite-time analysis of the multiarmed bandit problem
• Foundations of machine learning
• Intrinsic volumes and mixed volumes
• On transfinite Knuth-Bendix orders
• Paramodulation-based theorem proving
• Property invariant embedding for automated reasoning
• Reinforcement learning. An introduction
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

Cited in

(4)

• How much should this symbol weigh? A GNN-advised clause selection
• Learning guided automated reasoning: a brief survey
• When GNNs met a word equations solver: learning to rank equations
• Graph sequence learning for premise selection

Describes a project that uses

Uses Software

• ENIGMA
• Adam
• TPTP
• VAMPIRE

This page was built for publication: Neural precedence recommender

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