Learning to parse on aligned corpora (rough diamond)

DOI10.1007/978-3-319-22102-1_15MaRDI QIDQ2945635zbMATH OpenOpenAlexWikidataFDO

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

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) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Mathematical Knowledge Management
• Automating formalization by statistical and semantic parsing of mathematics
• Developing corpus-based translation methods between informal and formal mathematics: project description
• New Developments in Parsing Mizar
• Parsing and disambiguation of symbolic mathematics in the Naproche system

Cites work

• Dense sphere packings. A blueprint for formal proofs
• Developing corpus-based translation methods between informal and formal mathematics: project description
• Formal mathematics on display: a wiki for Flyspeck
• Hammering towards QED
• HOL(y)Hammer: online ATP service for HOL Light
• scientific article; zbMATH DE number 2190569 (Why is no real title available?)
• Overview and evaluation of premise selection techniques for large theory mathematics
• Recognition and parsing of context-free languages in time n3

Cited in

(6)

• Automating formalization by statistical and semantic parsing of mathematics
• From informal to formal proofs in Euclidean geometry
• Mathematical Knowledge Management
• Developing corpus-based translation methods between informal and formal mathematics: project description
• ProofLang: the language of arXiv proofs
• Translating SUMO-K to Higher-Order Set Theory

Describes a project that uses

Uses Software

• Flyspeck

This page was built for publication: Learning to parse on aligned corpora (rough diamond)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945635)