(Kaliszyk et al. 2017)[1]
TODO: REAL_NEGNEG (HOL theorem)??
Contents
Evaluation[]
Parse evaluation only[]
In Kaliszyk et al. 2017[]
- Sentences are shuffled
- 100-fold cross-validation
- Evaluate 20 highest-ranked parses
ATP evaluation[]
In Kaliszyk et al. 2017[]
- Make use of chronological order
- ...
Corpora[]
- 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[]
- Cezary Kaliszyk (Innsbruck)
- Josef Urban (Czech Technical University)
- Jirı Vyskocil (Czech Technical University)
Projects[]
References[]
- ↑ 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.
