MaLeCoP

swMATH7197MaRDI QIDQ19250FDOQ19250

Author name not available (Why is that?)

Official website: http://rd.springer.com/chapter/10.1007%2F978-3-642-22119-4_21

Described by source

• MaLeCoP. Machine learning connection prover

Cited In (35)

• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Fast and slow enigmas and parental guidance
• Vampire with a brain is a good ITP hammer
• Lemma Mining over HOL Light
• Portfolio theorem proving and prover runtime prediction for geometry
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• Internal guidance for Satallax
• 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
• MizarMode
• MPTP 0.2
• MoMM
• ileanCoP
• leanCoP
• Automated and human proofs in general mathematics: an initial comparison
• Overview and evaluation of premise selection techniques for large theory mathematics
• DeepMath
• TacticToe
• Automated reasoning service for HOL Light
• Theorem proving in large formal mathematics as an emerging AI field
• 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}\)
• Mizar: state-of-the-art and beyond
• 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
• TacticToe: learning to reason with HOL4 tactics

This page was built for software: MaLeCoP