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

Related Items (28)

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

This page was built for publication: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance