ML4PG in computer algebra verification

Jonathan Heras, Ekaterina Komendantskaya

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

    7 Citations (Scopus)


    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
    Number of pages5
    ISBN (Electronic)9783642393204
    ISBN (Print)9783642393198
    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

    Publication series

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


    ConferenceConferences on Intelligent Computer Mathematics: Calculemus 2013
    Abbreviated titleCICM 2013
    Country/TerritoryUnited Kingdom
    OtherHeld as Part of CICM 2013
    Internet address


    Dive into the research topics of 'ML4PG in computer algebra verification'. Together they form a unique fingerprint.

    Cite this