Jordan Normal Forms

MaRDI QIDQ40280swMATHFDO

Authors René Thiemann, Akihisa Yamada, Alexander Bentkamp

Publication date 21 August 2015

Official website https://www.isa-afp.org/entries/Jordan_Normal_Form.html

Cites work

• Arctic Termination ...Below Zero
• Certification of complexity proofs using CeTA
• Certification of Termination Proofs Using CeTA
• From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals
• Matrix interpretations for proving termination of term rewriting
• Matrix Theory

Cited in

(18)

• The matrix reproved (verification pearl)
• Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
• Certified quantum computation in Isabelle/HOL
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• QR Decomposition
• Perron Frobenius
• Algebraic Numbers
• Verified LLL
• Sturm-Tarski Theorem
• Groebner_Bases
• Deep_Learning
• Polynomials
• Group-Ring-Module
• Matrix_Tensor
• A verified efficient implementation of the LLL basis reduction algorithm
• Probabilistic_While
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning

This page was built for software: Jordan Normal Forms