Learning to Reason with HOL4 tactics

2 April 2018

Papers citing "Learning to Reason with HOL4 tactics"

9 / 9 papers shown

Title
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 145 3 0 18 Dec 2024
Internal Guidance for Satallax Michael Färber C. Brown LRM 30 26 0 30 May 2016
Premise Selection and External Provers for HOL4 Thibault Gauthier C. Kaliszyk 23 46 0 11 Sep 2015
Learning-assisted Theorem Proving with Millions of Lemmas C. Kaliszyk Josef Urban 59 47 0 11 Feb 2014
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 73 134 0 10 Oct 2013
Recycling Proof Patterns in Coq: Case Studies Jónathan Heras Ekaterina Komendantskaya 46 20 0 25 Jan 2013
BliStr: The Blind Strategymaker Josef Urban 45 65 0 12 Jan 2013
Machine Learning in Proof General: Interfacing Interfaces Ekaterina Komendantskaya Jónathan Heras G. Grov 58 56 0 14 Dec 2012
Learning-Assisted Automated Reasoning with Flyspeck C. Kaliszyk Josef Urban LRM 66 162 0 29 Nov 2012