Premise selection for mathematics by corpus analysis and kernel methods

DOI10.1007/s10817-013-9286-5zbMath1315.68217arXiv1108.3446OpenAlexW1982239968MaRDI QIDQ2352489

Daniel Kühlwein, Jesse Alama, Josef Urban, Tom Heskes, Evgeni Tsivtsivadze

Publication date: 2 July 2015

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

Full work available at URL: https://arxiv.org/abs/1108.3446

zbMATH Keywords

machine learningautomated theorem provingpremise selectionautomated reasoning in large theories

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

Related Items

MizAR 40 for Mizar 40 ⋮ Vampire with a brain is a good ITP hammer ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library ⋮ The role of entropy in guiding a connection prover ⋮ Eliminating models during model elimination ⋮ Learning theorem proving components ⋮ System Description: E.T. 0.1 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Hammer for Coq: automation for dependent type theory ⋮ Random Forests for Premise Selection ⋮ Lemmatization for Stronger Reasoning in Large Theories ⋮ Logical analysis of emotions in text from natural language ⋮ ATP and presentation service for Mizar formalizations ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Hierarchical invention of theorem proving strategies ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ 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 ⋮ Machine learning guidance for connection tableaux ⋮ mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library ⋮ Extending E Prover with Similarity Based Clause Selection Strategies ⋮ GRUNGE: a grand unified ATP challenge ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Mining State-Based Models from Proof Corpora ⋮ Guiding an automated theorem prover with neural rewriting ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10 ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• Coq
• Isabelle/HOL
• MPTP
• MPTP 0.2
• VAMPIRE
• SPASS
• Metis_
• Mizar
• z3
• HOL Light
• MML
• Sledgehammer
• Pegasos
• E Theorem Prover
• MaLARea
• PRMLT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MPTP-motivation, implementation, first experiments
• Pegasos: primal estimated sub-gradient solver for SVM
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• MPTP 0.2: Design, implementation, and initial experiments
• Obvious inferences
• Isabelle/HOL. A proof assistant for higher-order logic
• ATP and presentation service for Mizar formalizations
• Translating higher-order clauses to first-order clauses
• Automated and Human Proofs in General Mathematics: An Initial Comparison
• Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
• Co-Regularized Least-Squares for Label Ranking
• Automatic Proof and Disproof in Isabelle/HOL
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Sine Qua Non for Large Theory Reasoning
• Large Formal Wikis: Issues and Solutions
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
• Theory of Reproducing Kernels