ML4PG in computer algebra verification

Jonathan  Heras; Ekaterina  Komendantskaya

doi:10.1007/978-3-642-39320-4_28

ML4PG in computer algebra verification

Jonathan Heras, Ekaterina Komendantskaya

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

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 language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
Editors	Jacques Carette, David Aspinall , Christoph Lange, Petr Sojka, Wolfgang Windsteiger
Place of Publication	Berlin
Publisher	Springer
Pages	354-358
Number of pages	5
ISBN (Electronic)	9783642393204
ISBN (Print)	9783642393198
DOIs	https://doi.org/10.1007/978-3-642-39320-4_28
Publication status	Published - 2013
Event	Conferences on Intelligent Computer Mathematics: Calculemus 2013 - University of Bath in Building 8W, Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013 http://www.cicm-conference.org/2013/cicm.php

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	7961
ISSN (Print)	0302-9743

Conference

Conference	Conferences on Intelligent Computer Mathematics: Calculemus 2013
Abbreviated title	CICM 2013
Country/Territory	United Kingdom
City	Bath
Period	8/07/13 → 12/07/13
Other	Held as Part of CICM 2013
Internet address	http://www.cicm-conference.org/2013/cicm.php

Access to Document

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

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. Berlin : Springer , 2013. pp. 354-358 (Lecture notes in computer science).

@inproceedings{bcc694d6490c498eb3ce9f1bf851448d,

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

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 = "Carette, {Jacques } and {Aspinall }, {David } and Lange, {Christoph } and Sojka, {Petr } and Windsteiger, {Wolfgang }",

booktitle = "Intelligent Computer Mathematics",

note = "Conferences on Intelligent Computer Mathematics: Calculemus 2013, CICM 2013 ; Conference date: 08-07-2013 Through 12-07-2013",

url = "http://www.cicm-conference.org/2013/cicm.php",

}

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 , Berlin, pp. 354-358, Conferences on Intelligent Computer Mathematics: Calculemus 2013, Bath, United Kingdom, 8/07/13. 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. Berlin: Springer , 2013. p. 354-358 (Lecture notes in computer science; Vol. 7961).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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.

UR - http://www.scopus.com/inward/record.url?scp=84880711266&partnerID=8YFLogxK

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

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

M3 - Conference contribution

AN - SCOPUS:84880711266

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

CY - Berlin

T2 - Conferences on Intelligent Computer Mathematics: Calculemus 2013

Y2 - 8 July 2013 through 12 July 2013

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. Berlin: Springer . 2013. p. 354-358. (Lecture notes in computer science). doi: 10.1007/978-3-642-39320-4_28

ML4PG in computer algebra verification

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

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

Machine learning in Proof General: interfacing interfaces