No Cover Image

Book chapter 44 views

Concurrent Gaussian Elimination

Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo, Dieter Spreen, Hideki Tsuiki

Mathematics for Computation (M4C), Pages: 193 - 217

Swansea University Authors: Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

Abstract

Working in a semi-constructive logical system that supports the extraction of concurrent programs, we extract a program inverting non-singular real valued matrices from a constructive proof based on Gaussian elimination. Concurrency is used for efficient pivoting, that is, for finding an entry that...

Full description

Published in: Mathematics for Computation (M4C)
ISBN: 9789811245213 9789811245220
Published: Singapore WORLD SCIENTIFIC 2023
Online Access: https://doi.org/10.1142/12500
URI: https://cronfa.swan.ac.uk/Record/cronfa60609
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: Working in a semi-constructive logical system that supports the extraction of concurrent programs, we extract a program inverting non-singular real valued matrices from a constructive proof based on Gaussian elimination. Concurrency is used for efficient pivoting, that is, for finding an entry that is apart from zero in a non-null vector of real numbers.
Item Description: https://doi.org/10.1142/12500
Keywords: logic, proof theory, realisability, constructive mathematics, program extraction, concurrency, nondeteminism, Gaussian elimination, exact real number computation
College: Faculty of Science and Engineering
Start Page: 193
End Page: 217