Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description

DOI10.1007/978-3-319-08434-3_34zbMath1304.68172arXiv1405.3451OpenAlexW1509866286WikidataQ108482165 ScholiaQ108482165MaRDI QIDQ5495943

Josef Urban, Jiří Vyskočil, Cezary Kaliszyk, Herman Geuvers

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Related Items (5)

Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues ⋮ From informal to formal proofs in Euclidean geometry ⋮ Aligning concepts across proof assistant libraries ⋮ Learning to Parse on Aligned Corpora (Rough Diamond) ⋮ Automating formalization by statistical and semantic parsing of mathematics

Uses Software

• Mizar
• Flyspeck
• HOLyHammer

Cites Work

• MizAR 40 for Mizar 40
• A compendium of continuous lattices in MIZAR
• ATP and presentation service for Mizar formalizations
• HOL(y)Hammer: online ATP service for HOL Light
• Formal Mathematics on Display: A Wiki for Flyspeck

This page was built for publication: Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description