(Kaliszyk et al. 2017)[1]
TODO: REAL_NEGNEG (HOL theorem)??
Evaluation 
Edit
Parse evaluation only Edit
In Kaliszyk et al. 2017 Edit
- Sentences are shuffled
- 100-fold cross-validation
- Evaluate 20 highest-ranked parses
ATP evaluation Edit
In Kaliszyk et al. 2017 Edit
- Make use of chronological order
- ...
Corpora Edit
- Informalized Flyspeck (Kaliszyk et al. 2015[2])
?cited as additional annotation: T. Hales. Dense Sphere Packings: A Blueprint for Formal Proofs, volume 400 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2012
People Edit
- Cezary Kaliszyk (Innsbruck)
- Josef Urban (Czech Technical University)
- Jirı Vyskocil (Czech Technical University)
Projects Edit
References Edit
- ↑ Kaliszyk, C., Urban, J., & Vyskočil, J. (2017). Automating formalization by statistical and semantic parsing of mathematics. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10499 LNCS(714034), 12–27. http://doi.org/10.1007/978-3-319-66107-0_2
- ↑ C. Kaliszyk, J. Urban, and J. Vyskocil. Learning to parse on aligned corpora (rough diamond). In C. Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, volume 9236 of LNCS, pages 227–233. Springer, 2015.
