System Description: Statistical Parsing of Informalized Mizar Formulas
Cezary Kaliszyk, Josef Urban, Jiri Vyskocil · 2017
We describe a statistical system that learns parsing of ambiguous Mizar-like formulas from a large training corpus of aligned informal/formal formulas. We describe the methodology, the overall ideas, evaluate the performance of the system, and provide a web interface for using the system.