ML4PG in Computer Algebra Verification

Jonathan Heras, Ekaterina Komendantskaya

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library - a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationMKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
EditorsJacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger
PublisherSpringer
Pages354-358
Number of pages5
ISBN (Electronic)9783642393204
ISBN (Print)9783642393198
DOIs
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume7961
ISSN (Print)0302-9743

Fingerprint

Algebra
Learning systems

Keywords

  • ML4PG
  • Interactive Theorem Proving
  • Coq
  • SSReflect
  • Machine Learning
  • Clustering
  • CoqEAL

Cite this

Heras, J., & Komendantskaya, E. (2013). ML4PG in Computer Algebra Verification. In J. Carette, D. Aspinall, C. Lange, P. Sojka, & W. Windsteiger (Eds.), Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings (pp. 354-358). (Lecture Notes in Computer Science; Vol. 7961). Springer. https://doi.org/10.1007/978-3-642-39320-4_28
Heras, Jonathan ; Komendantskaya, Ekaterina. / ML4PG in Computer Algebra Verification. Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. editor / Jacques Carette ; David Aspinall ; Christoph Lange ; Petr Sojka ; Wolfgang Windsteiger. Springer, 2013. pp. 354-358 (Lecture Notes in Computer Science).
@inbook{e4737023178a4a2e9890c9d2a7c2b63a,
title = "ML4PG in Computer Algebra Verification",
abstract = "ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library - a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.",
keywords = "ML4PG, Interactive Theorem Proving, Coq, SSReflect, Machine Learning, Clustering, CoqEAL",
author = "Jonathan Heras and Ekaterina Komendantskaya",
year = "2013",
doi = "10.1007/978-3-642-39320-4_28",
language = "English",
isbn = "9783642393198",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "354--358",
editor = "Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger",
booktitle = "Intelligent Computer Mathematics",

}

Heras, J & Komendantskaya, E 2013, ML4PG in Computer Algebra Verification. in J Carette, D Aspinall, C Lange, P Sojka & W Windsteiger (eds), Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7961, Springer, pp. 354-358. https://doi.org/10.1007/978-3-642-39320-4_28

ML4PG in Computer Algebra Verification. / Heras, Jonathan; Komendantskaya, Ekaterina.

Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. ed. / Jacques Carette; David Aspinall; Christoph Lange; Petr Sojka; Wolfgang Windsteiger. Springer, 2013. p. 354-358 (Lecture Notes in Computer Science; Vol. 7961).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - ML4PG in Computer Algebra Verification

AU - Heras, Jonathan

AU - Komendantskaya, Ekaterina

PY - 2013

Y1 - 2013

N2 - ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library - a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.

AB - ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library - a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.

KW - ML4PG

KW - Interactive Theorem Proving

KW - Coq

KW - SSReflect

KW - Machine Learning

KW - Clustering

KW - CoqEAL

U2 - 10.1007/978-3-642-39320-4_28

DO - 10.1007/978-3-642-39320-4_28

M3 - Chapter

SN - 9783642393198

T3 - Lecture Notes in Computer Science

SP - 354

EP - 358

BT - Intelligent Computer Mathematics

A2 - Carette, Jacques

A2 - Aspinall, David

A2 - Lange, Christoph

A2 - Sojka, Petr

A2 - Windsteiger, Wolfgang

PB - Springer

ER -

Heras J, Komendantskaya E. ML4PG in Computer Algebra Verification. In Carette J, Aspinall D, Lange C, Sojka P, Windsteiger W, editors, Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Springer. 2013. p. 354-358. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-39320-4_28