zbMATH — the first resource for mathematics

ML4PG in computer algebra verification. (English) Zbl 1390.68780
Carette, Jacques (ed.) et al., 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 (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 354-358 (2013).
Summary: 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.
For the entire collection see [Zbl 1268.68008].

68W30 Symbolic computation and algebraic computation
68T05 Learning and adaptive systems in artificial intelligence
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI