1 citations · 1 across the 3 of their papers we have counts for
3 papers
cs.CL2016★ 1 cited
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
Cezary Kaliszyk, Josef Urban, Jiří Vyskočil
We study methods for automated parsing of informal mathematical expressions into formal ones, a main prerequisite for deep computer understanding of informal mathematical texts. We…
cs.LO2014
Certified Connection Tableaux Proofs for HOL Light and TPTP
Cezary Kaliszyk, Josef Urban, Jiri Vyskocil
In the recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 a…
cs.AI2014
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description
Cezary Kaliszyk, Josef Urban, Jiri Vyskocil +1
The goal of this project is to (i) accumulate annotated informal/formal mathematical corpora suitable for training semi-automated translation between informal and formal mathematic…