1 citations · 1 across the 5 of their papers we have counts for
5 papers
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
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…
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…
Matching concepts across HOL libraries
Thibault Gauthier, Cezary Kaliszyk
Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they…
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…