Fetching the paper…
Reading the bibliography…
We present ML4PG - a machine learning extension for Proof General.
Springer-Verlag, 10.1007/978-1-4757-1904-8
I. Joliffe (1986): Principal Components Analysis · 1904
Earlier work this paper cites.
Journal of Formalized Reasoning
G. Gonthier & A. Mahboubi (2010): An introduction to small scale reflection · 1979
Earlier work this paper cites.
Journal of Formalized Reasoning
A. Grabowski, A. Kornilowicz & A. Naumowicz (2010): Mizar in a nutshell · 1980
Earlier work this paper cites.
Inf. Comput
Thierry Coquand & Gérard P. Huet (1988): The Calculus of Constructions · 1988
Earlier work this paper cites.
Journal of Automated Reasoning
A. Bauer, E. M. Clarke & X. Zhao (1998): Analytica - an experiment in combining theorem proving and symbolic computation · 1998
Earlier work this paper cites.
Journal of Automated Reasoning
J. Harrison & L. Théry (1998): A skeptic approach to combining HOL and Maple · 1998
Earlier work this paper cites.
Technical Report, Technische Universitat Munchen
J. Denzinger, M. Fuchs, C. Goller & S. Schulz (1999): Learning from Previous Proof Experience: A Survey · 1999
Earlier work this paper cites.
Information and Computation
J. Denzinger & S. Schulz (2000): Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts · 1999
Earlier work this paper cites.
In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00)
D. Aspinall (2000): Proof General: A Generic Tool for Proof Development · 2000
Earlier work this paper cites.
Kluwer Academic Publishers
M. Kaufmann, P. Manolios & J S. Moore, editors (2000): Computer-Aided Reasoning: ACL2 Case Studies · 2000
Earlier work this paper cites.
Ph.D. thesis, University of Edinburgh
H. Duncan (2002): The use of Data-Mining for the Automatic Formation of Tactics · 2002
Earlier work this paper cites.
Technical Report
M. Jamnik, M. Kerber & C. Benzmller (2002): Automatic learning of proof methods in proof planning · 2002
Earlier work this paper cites.
Lecture Notes in Computer Science
T. Nipkow, L. C. Paulson & M. Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic · 2002
Earlier work this paper cites.
Artificial Intelligence Communications
A. Riazano & A. Voronkov (2002): The design and implementation of Vampire · 2002
Earlier work this paper cites.
In: 19th International Conference on Automated Deduction (CADE’2003)
L. Dixon & J. D. Fleuriot (2003): IsaPlanner: A Prototype Proof Planner in Isabelle · 2003
Earlier work this paper cites.
In: 2nd International Joint Conference on Automated Reasoning (IJCAR’04)
S. Schulz (2004): System description: E 0.81 · 2004
Earlier work this paper cites.
Cambridge University Press
D. Basin, A. Bundy, D. Hutter & A. Ireland (2005): Rippling: Meta-level Guidance for Mathematical Reasoning · 2005
Earlier work this paper cites.
Project description available at http://code.google.com/p/flyspeck/
T. Hales (2005): The Flyspeck Project fact sheet · 2005
Earlier work this paper cites.
Journal of Applied Logic
J. Urban (2006): MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics · 2005
Earlier work this paper cites.
IEEE Transactions on Neural Networks
R. Xu & D. Wunsch (2005): Survey of Clustering Algorithms · 2005
Earlier work this paper cites.
In: Post-Proceedings of the TYPES’04 International Conference
A. Asperti, F. Guidi, C. Sacerdoti Coen, E. Tassi & S. Zacchiroli (2006): A Content Based Mathematical Search Engine: Whelp · 2006
Cited alongside, same era.
Springer
C. Bishop (2006): Pattern Recognition and Machine Learning · 2006
Cited alongside, same era.
Available at http://yices.csl.sri.com/tool-paper.pdf
B. Dutertre & L. de Moura (2006): The Yices SMT solver · 2006
Cited alongside, same era.
In: 6th International workshop on the ACL2 theorem prover and its applications
W. A. Hunt & E. Reeber (2006): A SAT-based procedure for verifying finite state machines in ACL2 · 2006
Cited alongside, same era.
In: Eighth International Workshop on Termination, part of FLOC’06
M. Kaufmann, P. Manolios, J S. Moore & D. Vroon (2006): Integrating CCG analysis into ACL2 · 2006
Cited alongside, same era.
In: Mathematical User-Interfaces Workshop (MathUI’2006)
A. Mercer, A. Bundy, H. Duncan & D. Aspinall (2006): PG Tips: A Recommender System for an Interactive Theorem Prover · 2006
Journal of Automated Reasoning
M. Johansson, L. Dixon & A. Bundy (2011): Conjecture Synthesis for Inductive Theories · 2011
Later among the works it cites.
In: SIAM Conference on Data Mining (SDM’11)
E. Tsivtsivadze, J. Urban, H. Geuvers & T. Heskes (2011): Semantic Graph Kernels for Automated Reasoning · 2011
Later among the works it cites.
Dagstuhl Reports
A. Bundy, D. Hutter, C. B. Jones & J S. Moore (2012): AI meets Formal Software Development (Dagstuhl Seminar 12271) · 2012
Closest in time.
Technical Report
Coq · 2012
Closest in time.
In: ICML’12 worshop on Statistical Relational Learning
G. Grov, E. Komendantskaya & A. Bundy (2012): A Statistical Relational Learning Challenge - extracting proof strategies from exemplar proofs · 2012
Closest in time.
http://www.computing.dundee.ac.uk/staff/katya/ML4PG/
J. Heras & E. Komendantskaya (2012): ML4PG: machine learning interface for Proof General. Program files and user manual · 2012
Closest in time.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Journal of Automated Reasoning
J. Urban (2006): MPTP 0.2: Design, Implementation, and Initial Experiments · 2006
Cited alongside, same era.
In: 19th International Conference on Computer Aided Verification (CAV’07)
C. Barrett & C. Tinelli (2007): CVC3 · 2007
Cited alongside, same era.
Journal of Applied Logic
J. Meng & L. C. Paulson (2009): Lightweight relevance filtering for machine-generated resolution problems · 2007
Cited alongside, same era.
Notices of the American Mathematical Society
G. Gonthier (2008): Formal proof - The Four-Color Theorem · 2008
Cited alongside, same era.
In: 14th Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08)
L. M. de Moura & N. Bjorner (2008): Z3: An efficient SMT solver · 2008
Cited alongside, same era.
In: 4th International Joint Conference on Automated Reasoning (IJCAR’08)
J. Urban, G. Sutcliffe, P. Pudlák & J. Vyskocil (2008): MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance · 2008
Cited alongside, same era.
http://www.cs.utexas.edu/users/moore/acl2/current/ACCUMULATED-PERSISTENCE.html
M. Kaufmann & J S. Moore (2012): Accumulated persistence in ACL2 · 2012
Closest in time.
In: International Conference on Artificial Neural Networks (ICANN’12)
E. Komendantskaya & K. Lichota (2012): Neural Networks for Proof-Pattern Recognition · 2012
Closest in time.
In: 9th International Workshop On User Interfaces for Theorem Provers (UITP’10)
V. Komendantsky, A. Konovalov & S. Linton (2012): Interfacing Coq + SSReflect with GAP · 2012
Closest in time.
In: 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR’12)
D. Kuehlwein & J. Urban (2012): Learning from Multiple Proofs: first experiments · 2012
Closest in time.
In: 6th International Joint Conference on Automated Reasoning (IJCAR’12)
D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban & T. Heskes (2012): Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics · 2012
Closest in time.
The MathWorks Inc., Natick, Massachusetts
MATLAB (2012): version 7.14.0 (R2012a) · 2012
Closest in time.
Master’s thesis, University of Gothenburg, Sweden
D. Rosén (2012): Proving Equational Haskell Properties using Automated Theorem Provers · 2012
Closest in time.
Technical Report
Mathematical components team (2012): Formalization of the Odd Order theorem · 2012
Closest in time.
In: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13)
J. C. Blanchette, S. Böhme, A. Popescu & N. Smallbone (2013): Encoding monomorphic and polymorphic types · 2013
Closest in time.
In: 24th International Conference on Automated Deduction (CADE–24)
K. Claessen, M. Johansson, D. Rosén & N. Smallbone (2013): Automating Inductive Proofs using Theory Exploration · 2013
Closest in time.
In: Conferences on Intelligent Computer Mathematics (CICM’13)
J. Heras & E. Komendantskaya (2013): ML4PG in Computer Algebra Verification · 2013
Closest in time.
In: 4th Conference on Interactive Theorem Proving (ITP’13)
D. Kühlwein, J. C. Blanchette, C. Kaliszyk & J. Urban (2013): MaSh: Machine Learning for Sledgehammer · 2013
Closest in time.
Handbook of Automated Reasoning, Elsevier
C. Weidenbach (2001): Combining superposition, sorts and splitting , pp. 1965–2013 · 2013
Closest in time.