Natural Language Understanding Wiki
Advertisement

(Kaliszyk et al. 2017)[1]

TODO: REAL_NEGNEG (HOL theorem)??

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[]

  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.