ML4PG in computer algebra verification

DOI10.1007/978-3-642-39320-4_28MaRDI QIDQ2843038zbMATH OpenOpenAlexFDO

Authors Jónathan Heras, Ekaterina Komendantskaya

Publication date 9 August 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.6421

zbMATH Keywords

clusteringmachine learningCoqinteractive theorem provingSSReflectCoqEALML4PG

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Symbolic computation and algebraic computation (68W30)

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.

Recommendations

• Recycling proof patterns in Coq: case studies
• scientific article; zbMATH DE number 6528605
• Deepalgebra -- an outline of a program
• scientific article; zbMATH DE number 1194184
• Proof-pattern recognition and lemma discovery in ACL2

Cited in

(4)

• Mining state-based models from proof corpora
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• ML4PG
• Recycling proof patterns in Coq: case studies

Describes a project that uses

Uses Software

• Coq/SSReflect
• MaSh
• CoqEAL
• Coq

This page was built for publication: ML4PG in computer algebra verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843038)