Theorem proving in large formal mathematics as an emerging AI field
From MaRDI portal
Publication:4913871
DOI10.1007/978-3-642-36675-8_13zbMATH Open1276.68139arXiv1209.3914OpenAlexW2155552045MaRDI QIDQ4913871FDOQ4913871
Authors: Josef Urban, Jiří Vyskočil 
Publication date: 16 April 2013
Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)
Abstract: In the recent years, we have linked a large corpus of formal mathematics with automated theorem proving (ATP) tools, and started to develop combined AI/ATP systems working in this setting. In this paper we first relate this project to the earlier large-scale automated developments done by Quaife with McCune's Otter system, and to the discussions of the QED project about formalizing a significant part of mathematics. Then we summarize our adventure so far, argue that the QED dreams were right in anticipating the creation of a very interesting semantic AI field, and discuss its further research directions.
Full work available at URL: https://arxiv.org/abs/1209.3914
Recommendations
Cites Work
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Satallax: An Automatic Higher-Order Prover
- MaLeCoP. Machine learning connection prover
- The TPTP World -- infrastructure for automated reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- MPTP-motivation, implementation, first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- SRASS - A Semantic Relevance Axiom Selection System
- Isabelle/HOL. A proof assistant for higher-order logic
- Lightweight relevance filtering for machine-generated resolution problems
- On the rules of suppositions in formal logic
- ATP and presentation service for Mizar formalizations
- Premise selection for mathematics by corpus analysis and kernel methods
- Automated and human proofs in general mathematics: an initial comparison
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- On deciding satisfiability by theorem proving with speculative inferences
- Title not available (Why is that?)
- Mathematical Knowledge Management
- Computing small clause normal forms
- Superposition modulo linear arithmetic SUP(LA)
- Integrating Linear Arithmetic into Superposition Calculus
- Title not available (Why is that?)
- IeanCOP: lean connection-based theorem proving
- Automated deduction in von Neumann-Bernays-Gödel set theory
- A Wiki for Mizar: motivation, considerations, and initial prototype
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
Cited In (14)
- Set of support, demodulation, paramodulation: a historical perspective
- Machine learning for first-order theorem proving
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation
- Formalizing a fragment of combinatorics on words
- Deepalgebra -- an outline of a program
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Automated and human proofs in general mathematics: an initial comparison
- Learning-assisted theorem proving with millions of lemmas
- Advancing mathematics by guiding human intuition with AI
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Automating formalization by statistical and semantic parsing of mathematics
- Machine Learning for Inductive Theorem Proving
- MaLeCoP. Machine learning connection prover
Uses Software
This page was built for publication: Theorem proving in large formal mathematics as an emerging AI field
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913871)
