FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

DOI10.1007/978-3-662-48899-7_7MaRDI QIDQ3460043zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Recommendations

• MaLeCoP. Machine learning connection prover
• nanoCoP: a non-clausal connection prover
• IeanCOP: lean connection-based theorem proving
• scientific article; zbMATH DE number 6528605
• Deep network guided proof search
• Connection-driven inductive theorem proving
• A semi-automatic proof of strong connectivity
• The role of entropy in guiding a connection prover
• On the proof complexity of deep inference
• MleanCoP: a connection prover for first-order modal logic

Cited in

(18)

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

Describes a project that uses

Uses Software

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

This page was built for publication: FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

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