Formalization of operations of block matrix based on Coq

DOI10.13328/J.CNKI.JOS.006255MaRDI QIDQ3381519zbMATH OpenFDO

Authors Yingying Ma, Zhenwei Ma, Gang Chen

Publication date 29 September 2021

Full work available at URL https://doi.org/10.13328/J.CNKI.JOS.006255

zbMATH Keywords

deep learninghigher-order theorem provingblock matrixformal method

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Formalization of mathematics in connection with theorem provers (68V20) Special matrices (15B99)

Recommendations

• Formalization of function matrix theory in HOL
• Formalization of complex analysis and matrix theory
• scientific article; zbMATH DE number 2221149
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning

Cited in

(2)

• A framework for formal verification of robot kinematics
• Integration of multiple formal matrix models in Coq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formalization of operations of block matrix based on Coq

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