FANDOM


(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

  1. 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
  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.