Projects per year
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.
Original language | English |
---|---|
Pages (from-to) | 15-41 |
Number of pages | 26 |
Journal | Electronic Proceedings in Theoretical Computer Science |
Volume | 118 |
DOIs | |
Publication status | Published - 2013 |
Event | Proceedings of 10th International Workshop on User Interfaces for Theorem Provers - Bremen, Germany Duration: 11 Jul 2012 → 11 Jul 2012 |
Keywords
- Interactive Theorem Proving, User Interfaces, Proof General, Coq, SSReflect, Machine Learning, Clustering.
Fingerprint Dive into the research topics of 'Machine learning in Proof General: interfacing interfaces'. Together they form a unique fingerprint.
Projects
- 1 Finished
-
Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)
Komendantskaya, E.
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research
Research Output
- 1 Conference contribution
-
ML4PG in computer algebra verification
Heras, J. & Komendantskaya, E., 2013, Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Carette, J., Aspinall, D., Lange, C., Sojka, P. & Windsteiger, W. (eds.). Berlin: Springer , p. 354-358 5 p. (Lecture notes in computer science; vol. 7961).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
7 Citations (Scopus)