149 citations · 825 across the 48 of their papers we have counts for
Showing 2014 · cs.LOShow all
2 papers · 2 filters
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
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…