Machine learning in Proof General

Ekaterina Komendantskaya, Jonathan Heras, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Downloads (Pure)

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 languageEnglish
Title of host publicationProceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012)
PublisherOpen Publishing Association
Pages15-41
Number of pages27
DOIs
Publication statusPublished - 2013

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume118
ISSN (Print)2075-2180

Keywords

  • Interactive Theorem Proving
  • User Interfaces
  • Proof General
  • Coq
  • SSReflec
  • Machine Learning
  • Clustering

Fingerprint Dive into the research topics of 'Machine learning in Proof General'. Together they form a unique fingerprint.

  • Cite this

    Komendantskaya, E., Heras, J., & Grov, G. (2013). Machine learning in Proof General. In Proceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012) (pp. 15-41). (Electronic Proceedings in Theoretical Computer Science; Vol. 118). Open Publishing Association. https://doi.org/10.4204/EPTCS.118.2