Faster Smarter Induction in Isabelle/HOL

19 September 2020

Papers citing "Faster Smarter Induction in Isabelle/HOL"

15 / 15 papers shown

Title
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq Lasse Blaauwbroek Josef Urban H. Geuvers 20 23 0 31 Jul 2020
Towards United Reasoning for Automatic Induction in Isabelle/HOL Yutaka Nagashima LRM AI4CE 15 2 0 25 May 2020
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek Josef Urban H. Geuvers 84 24 0 20 Mar 2020
Stateful Premise Selection by Recurrent Neural Networks Bartosz Piotrowski Josef Urban LRM 24 21 0 11 Mar 2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Jan Jakubuv Karel Chvalovský Miroslav Olsák Bartosz Piotrowski Martin Suda Josef Urban 38 44 0 13 Feb 2020
Graph Representations for Higher-Order Logic and Theorem Proving Aditya Sanjay Paliwal Sarah M. Loos M. Rabe Kshitij Bansal Christian Szegedy AI4CE NoLa 113 97 0 24 May 2019
Learning to Prove Theorems via Interacting with Proof Assistants Kaiyu Yang Jia Deng AIMat LRM 86 144 0 21 May 2019
Towards Evolutionary Theorem Proving for Isabelle/HOL Yutaka Nagashima 15 8 0 17 Apr 2019
PaMpeR: Proof Method Recommendation System for Isabelle/HOL Yutaka Nagashima Yilun He 42 24 0 19 Jun 2018
TacticToe: Learning to Prove with Tactics Thibault Gauthier C. Kaliszyk Josef Urban Ramana Kumar Michael Norrish 45 53 0 02 Apr 2018
Learning to Reason with HOL4 tactics Thibault Gauthier C. Kaliszyk Josef Urban 43 77 0 02 Apr 2018
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving C. Kaliszyk François Chollet Christian Szegedy 23 82 0 01 Mar 2017
Deep Network Guided Proof Search Sarah M. Loos G. Irving Christian Szegedy C. Kaliszyk AIMat 51 158 0 24 Jan 2017
Automation of Mathematical Induction as part of the History of Logic J. Strother Claus-Peter Wirth AI4CE 62 14 0 24 Sep 2013
Isabelle/jEdit --- a Prover IDE within the PIDE framework M. Wenzel VLM 60 72 0 14 Jul 2012