### Abstract

We provide the operations of matrix addition, multiplication, transposition, and matrix comparisons as executable functions over ordered semirings. Moreover, it is proven that strongly normalizing (monotone) orders can be lifted to strongly normalizing (monotone) orders over matrices. We further show that the standard semirings over the naturals, integers, and rationals, as well as the arctic semirings satisfy the axioms that are required by our matrix theory. Our formalization is part of the CeTA system which contains several termination techniques. The provided theories have been essential to formalize matrix-interpretations and arctic interpretations.

### License

GNU Lesser General Public License (LGPL)

### History

September 17, 2010
  Moved theory on arbitrary (ordered) semirings to Abstract Rewriting.

### Topics

- Computer science/Data structures

### Session Matrix

- Utility
- Ordered_Semiring
- Matrix_Legacy

### Depends on

- Abstract Rewriting

### Used by

- A Formalization of Knuth–Bendix Orders
- Polynomial Factorization
- Tensor Product of Matrices
- Executable Transitive Closures of Finite Relations
- Executable Multivariate Polynomials

## Cite

×

Matrix-AFP

    @article{Matrix-AFP,
      author  = {Christian Sternagel and René Thiemann},
      title   = {Executable Matrix Operations on Matrices of Arbitrary Dimensions},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/Matrix.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Jun 17, 2010 : Isabelle2009-1