Machine Learning in Proof General: Interfacing Interfaces
Artificial Intelligence
2013-07-09 v2 Machine Learning
Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1212.3618,
title = {Machine Learning in Proof General: Interfacing Interfaces},
author = {Ekaterina Komendantskaya and Jónathan Heras and Gudmund Grov},
journal= {arXiv preprint arXiv:1212.3618},
year = {2013}
}
Comments
In Proceedings UITP 2012, arXiv:1307.1528