Automating formalization by statistical and semantic parsing of mathematics
From MaRDI portal
Publication:1687711
DOI10.1007/978-3-319-66107-0_2zbMath1483.68490OpenAlexW2746433573WikidataQ108482124 ScholiaQ108482124MaRDI QIDQ1687711
Josef Urban, Jiří Vyskočil, Cezary Kaliszyk
Publication date: 4 January 2018
Full work available at URL: https://zenodo.org/record/1227170
Learning and adaptive systems in artificial intelligence (68T05) Natural language processing (68T50) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (2)
From informal to formal proofs in Euclidean geometry ⋮ Automating formalization by statistical and semantic parsing of mathematics
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Commutative algebra in the Mizar system
- Automating formalization by statistical and semantic parsing of mathematics
- A compendium of continuous lattices in MIZAR
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Formal Mathematics on Display: A Wiki for Flyspeck
- A Language of Patterns for Subterm Selection
- Learning to Parse on Aligned Corpora (Rough Diamond)
- Packaging Mathematical Structures
- A Declarative Language for the Coq Proof Assistant
- The Isabelle Framework
- Constructive Type Classes in Isabelle
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Hammering towards QED
- A Machine-Checked Proof of the Odd Order Theorem
- Matching Concepts across HOL Libraries
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
- Recognition and parsing of context-free languages in time n3
This page was built for publication: Automating formalization by statistical and semantic parsing of mathematics
