MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance

DOI10.1007/978-3-540-71070-7_37zbMath1165.68434OpenAlexW1623345509MaRDI QIDQ3541722

Pavel Pudlák, Josef Urban, Jiří Vyskočil, Geoff Sutcliffe

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_37

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

Related Items

ENIGMA: efficient learning-based inference guiding machine, MizAR 40 for Mizar 40, Make E Smart Again (Short Paper), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Prolog Technology Reinforcement Learning Prover, Mizar: State-of-the-art and Beyond, Towards finding longer proofs, The role of entropy in guiding a connection prover, Automated Reasoning in the Wild, A learning-based fact selector for Isabelle/HOL, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, Alien coding, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Lemmatization for Stronger Reasoning in Large Theories, ATP and presentation service for Mizar formalizations, Learning-assisted theorem proving with millions of lemmas, Hammering Mizar by Learning Clause Guidance (Short Paper)., MaLeCoP Machine Learning Connection Prover, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Premise Selection in the Naproche System, HOL(y)Hammer: online ATP service for HOL Light, Machine learning guidance for connection tableaux, Sine Qua Non for Large Theory Reasoning, Learning2Reason, Towards the automatic mathematician, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• MPTP
• E Theorem Prover
• MaLARea

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A relevance restriction strategy for automated deduction
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• MPTP 0.2: Design, implementation, and initial experiments
• The TPTP problem library. CNF release v1. 2. 1
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• Translating higher-order clauses to first-order clauses
• SRASS - A Semantic Relevance Axiom Selection System
• Automated Reasoning
• Controlled use of clausal lemmas in connection tableau calculi