Machine learning in Proof General: interfacing interfaces

Ekaterina Komendantskaya; Jonathan Heras; Gudmund Grov

doi:10.4204/EPTCS.118.2

Machine learning in Proof General: interfacing interfaces

Ekaterina Komendantskaya, Jonathan Heras, Gudmund Grov

Research output: Contribution to journal › Article › peer-review

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	https://doi.org/10.4204/EPTCS.118.2
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, SSReﬂect, Machine Learning, Clustering.

Access to Document

10.4204/EPTCS.118.2

Embargoed Document

ML4PG
Submitted manuscript, 855 KB
Embargo ends: 31/12/99

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

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)

Cite this

@article{b97c2bdb80dd43ffb59e556b2b683612,

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.",

keywords = "Interactive Theorem Proving, User Interfaces, Proof General, Coq, SSReﬂect, Machine Learning, Clustering.",

author = "Ekaterina Komendantskaya and Jonathan Heras and Gudmund Grov",

year = "2013",

doi = "10.4204/EPTCS.118.2",

language = "English",

volume = "118",

pages = "15--41",

journal = "Electronic Proceedings in Theoretical Computer Science",

issn = "2075-2180",

publisher = "Open Publishing Association",

note = "Proceedings of 10th International Workshop on User Interfaces for Theorem Provers ; Conference date: 11-07-2012 Through 11-07-2012",

}

TY - JOUR

T1 - Machine learning in Proof General

T2 - Proceedings of 10th International Workshop on User Interfaces for Theorem Provers

AU - Komendantskaya, Ekaterina

AU - Heras, Jonathan

AU - Grov, Gudmund

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

KW - Interactive Theorem Proving, User Interfaces, Proof General, Coq, SSReﬂect, Machine Learning, Clustering.

U2 - 10.4204/EPTCS.118.2

DO - 10.4204/EPTCS.118.2

M3 - Article

VL - 118

SP - 15

EP - 41

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

Y2 - 11 July 2012 through 11 July 2012

ER -

Machine learning in Proof General: interfacing interfaces

Abstract

Keywords

Access to Document

Embargoed Document

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Research output

ML4PG in computer algebra verification

Cite this