Contents

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 sho...

Full description

Bibliographic Details
Main Authors: Christian Sternagel, René Thiemann
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: 2013
Subjects:
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9250
http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.400.9250
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.400.9250 2023-05-15T14:49:52+02:00 Contents Christian Sternagel René Thiemann The Pennsylvania State University CiteSeerX Archives 2013 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9250 http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9250 http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf text 2013 ftciteseerx 2016-01-08T02:48:37Z 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 was performed as part of the IsaFoR/CeTA-system [3] 1 which contains several termination techniques. The provided theories have been essential to formalize matrix-interpretations [1] and arctic interpretations [2]. A short description of this formalization can be found in [4]. Text Arctic Unknown Arctic
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description 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 was performed as part of the IsaFoR/CeTA-system [3] 1 which contains several termination techniques. The provided theories have been essential to formalize matrix-interpretations [1] and arctic interpretations [2]. A short description of this formalization can be found in [4].
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Christian Sternagel
René Thiemann
spellingShingle Christian Sternagel
René Thiemann
Contents
author_facet Christian Sternagel
René Thiemann
author_sort Christian Sternagel
title Contents
title_short Contents
title_full Contents
title_fullStr Contents
title_full_unstemmed Contents
title_sort contents
publishDate 2013
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9250
http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf
geographic Arctic
geographic_facet Arctic
genre Arctic
genre_facet Arctic
op_source http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9250
http://afp.sourceforge.net/browser_info/current/HOL/Matrix/document.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766320952623235072