HOL(y)Hammer: Online ATP Service for HOL Light

19 September 2013

Papers citing "HOL(y)Hammer: Online ATP Service for HOL Light"

8 / 8 papers shown

Title
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 73 134 0 10 Oct 2013
Lemma Mining over HOL Light C. Kaliszyk Josef Urban 38 12 0 10 Oct 2013
BliStr: The Blind Strategymaker Josef Urban 47 65 0 12 Jan 2013
WorkingWiki: a MediaWiki-based platform for collaborative research L. Worden SyDa 48 3 0 10 Dec 2012
Learning-Assisted Automated Reasoning with Flyspeck C. Kaliszyk Josef Urban LRM 68 162 0 29 Nov 2012
ATP and Presentation Service for Mizar Formalizations Josef Urban P. Rudnicki G. Sutcliffe LRM 44 66 0 03 Sep 2011
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods Jesse Alama Tom Heskes D. Kühlwein Evgeni Tsivtsivadze Josef Urban LRM 73 146 0 17 Aug 2011
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar Josef Urban G. Sutcliffe LRM 70 36 0 25 May 2010