Abstract

We describe a statistical system that learns parsing of ambiguous Mizar-like formulas from a large training corpus of aligned informal/formal formulas. We describe the methodology and the overall ideas, evaluate the performance of the system, and provide a public web interface for using the system.

BibTeX

@Article{ckjujv-synasc17,
  author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title = {System Description: Statistical Parsing of Informalized {M}izar Formulas},
  editor = {Tudor Jebelean, Viorel Negru, Dana Petcu, Daniela Zaharie, Tetsuo Ida, Stephen M. Watt},
  booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017},
  year = {2017},
  publisher = {{IEEE} Computer Society},
  pages = {169--172}
}