Machine learning in Proof General: interfacing interfaces

Ekaterina Komendantskaya, Jonathan Heras, Gudmund Grov

    Research output: Contribution to journalArticlepeer-review


    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 languageEnglish
    Pages (from-to)15-41
    Number of pages26
    JournalElectronic Proceedings in Theoretical Computer Science
    Publication statusPublished - 2013
    EventProceedings of 10th International Workshop on User Interfaces for Theorem Provers - Bremen, Germany
    Duration: 11 Jul 201211 Jul 2012


    • Interactive Theorem Proving, User Interfaces, Proof General, Coq, SSReflect, Machine Learning, Clustering.


    Dive into the research topics of 'Machine learning in Proof General: interfacing interfaces'. Together they form a unique fingerprint.
    • 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 proceedingConference contribution

      7 Citations (Scopus)

    Cite this