MaLeCoP Machine Learning Connection Prover

DOI10.1007/978-3-642-22119-4_21zbMath1332.68206OpenAlexW1573726182MaRDI QIDQ3010374

No author found.

Publication date: 1 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22119-4_21

Mathematics Subject Classification ID

Related Items (20)

ENIGMA: efficient learning-based inference guiding machine ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Mizar: State-of-the-art and Beyond ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The role of entropy in guiding a connection prover ⋮ Efficient Low-Level Connection Tableaux ⋮ CoProver: a recommender system for proof construction ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ Internal Guidance for Satallax ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ MaLeCoP ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• MPTP 0.2
• VAMPIRE
• MoMM
• MML
• leanCoP
• ileanCoP
• E Theorem Prover
• MaLARea

Cites Work

• Unnamed Item
• Unnamed Item
• MPTP 0.2: Design, implementation, and initial experiments
• Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
• IeanCOP: lean connection-based theorem proving
• Translating higher-order clauses to first-order clauses
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Restricting backtracking in connection calculi
• Sine Qua Non for Large Theory Reasoning
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library

This page was built for publication: MaLeCoP Machine Learning Connection Prover