Theorem proving in large formal mathematics as an emerging AI field
From MaRDI portal
Publication:4913871
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 158462 (Why is no real title available?)
- scientific article; zbMATH DE number 1951640 (Why is no real title available?)
- A Wiki for Mizar: motivation, considerations, and initial prototype
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- ATP and presentation service for Mizar formalizations
- Automated and human proofs in general mathematics: an initial comparison
- Automated deduction in von Neumann-Bernays-Gödel set theory
- Computing small clause normal forms
- IeanCOP: lean connection-based theorem proving
- Integrating Linear Arithmetic into Superposition Calculus
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Lightweight relevance filtering for machine-generated resolution problems
- MPTP 0.2: Design, implementation, and initial experiments
- MPTP-motivation, implementation, first experiments
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- MaLeCoP. Machine learning connection prover
- Mathematical Knowledge Management
- On deciding satisfiability by theorem proving with speculative inferences
- On the rules of suppositions in formal logic
- Premise selection for mathematics by corpus analysis and kernel methods
- SRASS - A Semantic Relevance Axiom Selection System
- Satallax: An Automatic Higher-Order Prover
- Superposition modulo linear arithmetic SUP(LA)
- The TPTP World -- infrastructure for automated reasoning
Cited in
(15)- 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
- A study of continuous vector representations for theorem proving
- 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
Describes a project that uses
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)
