149 citations · 563 across the 54 of their papers we have counts for
7 papers · 1 filter
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…
Machine Learning of Coq Proof Guidance: First Experiments
Cezary Kaliszyk, Lionel Mamane, Josef Urban
We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependenci…
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban
This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness o…
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…
Learning-assisted Theorem Proving with Millions of Lemmas
Cezary Kaliszyk, Josef Urban
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informa…