ML4PG in computer algebra verification

Jonathan Heras, Ekaterina Komendantskaya

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

    4 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 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
    Place of PublicationBerlin
    PublisherSpringer
    Pages354-358
    Number of pages5
    ISBN (Electronic)9783642393204
    ISBN (Print)9783642393198
    DOIs
    Publication statusPublished - 2013
    EventConferences on Intelligent Computer Mathematics: Calculemus 2013 - University of Bath in Building 8W, Bath, United Kingdom
    Duration: 8 Jul 201312 Jul 2013
    http://www.cicm-conference.org/2013/cicm.php

    Publication series

    NameLecture notes in computer science
    PublisherSpringer
    Volume7961
    ISSN (Print)0302-9743

    Conference

    ConferenceConferences on Intelligent Computer Mathematics: Calculemus 2013
    Abbreviated titleCICM 2013
    CountryUnited Kingdom
    CityBath
    Period8/07/1312/07/13
    OtherHeld as Part of CICM 2013
    Internet address

      Fingerprint

    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