Theorem Proving in Large Formal Mathematics as an Emerging AI Field
From MaRDI portal
Publication:4913871
DOI10.1007/978-3-642-36675-8_13zbMath1276.68139arXiv1209.3914OpenAlexW2155552045MaRDI QIDQ4913871
Publication date: 16 April 2013
Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1209.3914
Related Items (8)
Deepalgebra -- an outline of a program ⋮ MizAR 40 for Mizar 40 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Formalizing a fragment of combinatorics on words ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On deciding satisfiability by theorem proving with speculative inferences
- MPTP-motivation, implementation, first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- Lightweight relevance filtering for machine-generated resolution problems
- Automated deduction in von Neumann-Bernays-Gödel set theory
- IeanCOP: lean connection-based theorem proving
- Isabelle/HOL. A proof assistant for higher-order logic
- 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
- Satallax: An Automatic Higher-Order Prover
- MaLeCoP Machine Learning Connection Prover
- The TPTP World – Infrastructure for Automated Reasoning
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- Integrating Linear Arithmetic into Superposition Calculus
- SRASS - A Semantic Relevance Axiom Selection System
- Superposition Modulo Linear Arithmetic SUP(LA)
- Mathematical Knowledge Management
This page was built for publication: Theorem Proving in Large Formal Mathematics as an Emerging AI Field
