MaLeCoP

swMATH7197MaRDI QIDQ19250FDOQ19250

Author name not available (Why is that?)

Described by source

• MaLeCoP Machine Learning Connection Prover

Cited In (28)

• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Fast and slow enigmas and parental guidance
• Vampire with a brain is a good ITP hammer
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• Lemma Mining over HOL Light
• Portfolio theorem proving and prover runtime prediction for geometry
• Mizar: State-of-the-art and Beyond
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• The role of entropy in guiding a connection prover
• 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
• Monte Carlo tableau proof search
• TacticToe: Learning to Reason with HOL4 Tactics
• Internal Guidance for Satallax
• Efficient Low-Level Connection Tableaux
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted theorem proving with millions of lemmas
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Automated Reasoning Service for HOL Light
• Automated and Human Proofs in General Mathematics: An Initial Comparison
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• Prolog Technology Reinforcement Learning Prover
• ProofWatch: watchlist guidance for large theories in E
• ATPboost: learning premise selection in binary setting with ATP feedback
• Hammering towards QED
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search

This page was built for software: MaLeCoP