44 citations · 111 across the 15 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.AI2015★ 34 cited
Premise Selection and External Provers for HOL4
Thibault Gauthier, Cezary Kaliszyk
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof as…
cs.AI2015★ 1 cited
Sharing HOL4 and HOL Light proof knowledge
Thibault Gauthier, Cezary Kaliszyk
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing form…