activity
20142023
most citedSemantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving

1 citations · 1 across the 5 of their papers we have counts for

collaborators
Showing cs.LOShow all

2 papers · 1 filter

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.LO2014

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…