The goal of this project is to (i) accumulate annotated informal/formal mathematical corpora suitable for training semi-automated translation between informal and formal mathematics by statistical machine-translation methods, (ii) to develop such methods oriented at the formalization task, and in particular (iii) to combine such methods with learning-assisted automated reasoning that will serve as a strong semantic component. We describe these ideas, the initial set of corpora, and some initial experiments done over them.
|Title of host publication||Intelligent Computer Mathematics (International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings)|
|Editors||S.M. Watt, J.H. Davenport, A.P. Sexton, P. Sojka, J. Urban|
|Place of Publication||Berlin|
|Publication status||Published - 2014|
|Name||Lecture Notes in Computer Science|