Learning to Parse on Aligned Corpora (Rough Diamond)

DOI10.1007/978-3-319-22102-1_15zbMath1465.68287OpenAlexW2232826555WikidataQ108482147 ScholiaQ108482147MaRDI QIDQ2945635

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

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/143744

Mathematics Subject Classification ID

Natural language processing (68T50) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

From informal to formal proofs in Euclidean geometry ⋮ Automating formalization by statistical and semantic parsing of mathematics

Uses Software

• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• HOL(y)Hammer: online ATP service for HOL Light
• Formal Mathematics on Display: A Wiki for Flyspeck
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• Hammering towards QED
• 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: Learning to Parse on Aligned Corpora (Rough Diamond)