Paper Info
Title
Machine Learning In Proof General: Interfacing Interfaces
Abstract
We present ML4PG-a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.
Year
DOI
Venue
2013
10.4204/EPTCS.118.2
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Keywords
Field
DocType
Interactive Theorem Proving, User Interfaces, Proof General, Coq, SSReflect, Machine Learning, Clustering
Computer-assisted proof,MATLAB,Computer science,Automated proof checking,Interfacing,Theoretical computer science,Mathematical proof,Tree structure,Artificial intelligence,Cluster analysis,Machine learning,Proof assistant
Journal
Issue
ISSN
Citations 
118
2075-2180
11
PageRank 
References 
Authors
0.64
37
3
Name
Order
Citations
PageRank
Ekaterina Komendantskaya115022.66
Jónathan Heras29423.31
Gudmund Grov310017.38