Neural precedence recommender

DOI10.1007/978-3-030-79876-5_30OpenAlexW3182454636MaRDI QIDQ2055885

Martin Suda, Filip Bártek

Publication date: 1 December 2021

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)

Uses Software

• VAMPIRE
• TPTP
• Adam
• ENIGMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Faster, higher, stronger: E 2.3
• AVATAR: The Architecture for First-Order Theorem Provers
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• On Transfinite Knuth-Bendix Orders
• Automated Deduction – CADE-20
• Finite-time analysis of the multiarmed bandit problem