FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

DOI10.1007/978-3-662-48899-7_7zbMath1471.68312OpenAlexW2257927474WikidataQ108482154 ScholiaQ108482154MaRDI QIDQ3460043

Cezary Kaliszyk, Josef Urban

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-48899-7_7

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

ENIGMA: efficient learning-based inference guiding machine, Prolog Technology Reinforcement Learning Prover, Portfolio theorem proving and prover runtime prediction for geometry, Towards finding longer proofs, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, The role of entropy in guiding a connection prover, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics, Craig interpolation with clausal first-order tableaux, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, CoProver: a recommender system for proof construction, Hammering Mizar by Learning Clause Guidance (Short Paper)., TacticToe: learning to prove with tactics, Machine learning guidance for connection tableaux, nanoCoP: A Non-clausal Connection Prover, Internal Guidance for Satallax, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), FEMaLeCoP

Uses Software

• Mizar
• HOL Light
• Sledgehammer
• MaLeCoP
• MaSh
• leanCoP
• Flyspeck