Abstract

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.

BibTeX

@inproceedings{CKJUJVHG-CICM14,
  author      = "Cezary Kaliszyk and Josef Urban and Ji\c{r}\'i
                 Vysko\c{c}il and Herman Geuvers",
  title       = "Developing Corpus-based Translation Methods between
                 Informal and Formal Mathematics",
  booktitle   = "Proceedings of the 7th Conference on Intelligent Computer
                 Mathematics",
  editor      = "Stephen Watt and James Davenport and Alan Sexton and
                 Petr Sojka and Josef Urban",
  series      = "Lecture Notes in Computer Science",
  volume      = 8543,
  pages       = "435--439",
  publisher   = "Springer-Verlag",
  year        = 2014,
  doi         = "10.1007/978-3-319-08434-3_34"
}