Fetching the paper…
Reading the bibliography…
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover.
A statistical interpretation of term specificity and its application in retrieval
Karen Spärck Jones · 1972
Earlier work this paper cites.
The distance-weighted k-nearest-neighbor rule
Sahibsingh A. Dudani · 1976
Earlier work this paper cites.
The use of explicit plans to guide inductive proofs
Alan Bundy · 1988
Earlier work this paper cites.
The oyster-clam system
Alan Bundy, Frank van Harmelen, Christian Horn, and Alan Smaill · 1990
Earlier work this paper cites.
Recording and checking HOL proofs
Wai Wong · 1995
Earlier work this paper cites.
Omega: Towards a mathematical assistant
Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, and Volker Sorge · 1997
Earlier work this paper cites.
A tactic language for the system Coq
David Delahaye · 2000
Earlier work this paper cites.
Hol - a machine oriented formulation of higher order logic, 2001
Mike Gordon · 2001
Earlier work this paper cites.
E - a brainiac theorem prover
Stephan Schulz · 2002
Earlier work this paper cites.
IsaPlanner: A prototype proof planner in Isabelle
Lucas Dixon and Jacques D. Fleuriot · 2003
Earlier work this paper cites.
First-order proof tactics in higher-order logic theorem provers
Joe Hurd · 2003
Earlier work this paper cites.
Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions
Yves Bertot and Pierre Castéran · 2004
Earlier work this paper cites.
MPTP - Motivation, Implementation, First Experiments
Josef Urban · 2004
Earlier work this paper cites.
Malarea: a metasystem for automated reasoning in large theories
Josef Urban · 2007
Cited alongside, same era.
Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings
Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors · 2008
Cited alongside, same era.
HOL Light: An overview
John Harrison · 2009
Cited alongside, same era.
MaLeCoP Machine Learning Connection Prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Cited alongside, same era.
A survey of Monte Carlo tree search methods
Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton · 2012
Cited alongside, same era.
Machine learning in Proof General: Interfacing interfaces
Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov · 2012
Premise selection and external provers for HOL4
Thibault Gauthier and Cezary Kaliszyk · 2015
Later among the works it cites.
SEPIA: search for proofs using inferred automata
Thomas Gransden, Neil Walkinshaw, and Rajeev Raman · 2015
Later among the works it cites.
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Cezary Kaliszyk and Josef Urban · 2015
Later among the works it cites.
MizAR 40 for Mizar 40
Cezary Kaliszyk and Josef Urban · 2015
Later among the works it cites.
Hammering towards QED
Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, and Josef Urban · 2016
Later among the works it cites.
A learning-based fact selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban · 2016
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Standalone tactics using OpenTheory
Ramana Kumar and Joe Hurd · 2012
Cited alongside, same era.
Reducing higher-order theorem proving to a sequence of SAT problems
Chad E. Brown · 2013
Cited alongside, same era.
Stronger automation for Flyspeck by feature weighting and strategy evolution
Cezary Kaliszyk and Josef Urban · 2013
Cited alongside, same era.
ATP and presentation service for Mizar formalizations
Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe · 2013
Cited alongside, same era.
Recycling proof patterns in Coq: Case studies
Jónathan Heras and Ekaterina Komendantskaya · 2014
Cited alongside, same era.
Learning-assisted automated reasoning with Flyspeck
Cezary Kaliszyk and Josef Urban · 2014
Cited alongside, same era.
Internal guidance for Satallax
Michael Färber and Chad E. Brown · 2016
Later among the works it cites.
Eisbach: A proof method language for Isabelle
Daniel Matichuk, Toby Murray, and Makarius Wenzel · 2016
Later among the works it cites.
TacticToe: Learning to reason with HOL4 tactics
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2017
Later among the works it cites.
A proof strategy language and proof script generation for Isabelle/HOL
Yutaka Nagashima and Ramana Kumar · 2017
Later among the works it cites.
Mastering the game of go without human knowledge
David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, Yutian Chen, Timothy Lillicrap, Fan Hui, Laurent Sifre, George van den Driessche, Thore Graepel, and Demis Hassabis · 2017
Later among the works it cites.
Adapting proof automation to adapt proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman · 2018
Closest in time.