Numerical MMATh Verified essential algorithms for solving differential equations
Numerical MMATh Verified essential algorithms for solving differential equations
No Thumbnail Available
Date
2019
Authors
Editors
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
URI (citable link)
International patent number
Link to the license
EU project number
Project
Open Access publication
Collections
Title in another language
Publication type
Dissertation
Publication status
Published
Published in
Abstract
Summary in another language
Wie lässt sich mathematisch beweisen, dass numerische Algorithmen korrekt arbeiten? Eine mögliche Antwort auf diese Kernfrage gibt die vorliegende Arbeit. Dazu wird ein mathematisches Modell numerischer Algorithmen vorgestellt.
Durch eine präzise Definition von Darstellungen und Algorithmen können Rechnerobjekte und mathematische Objekte miteinander verbunden werden. Damit wird die Lücke zwischen mathematischer Theorie und Implementierung verringert. Es ist dann möglich, im Sinne von deduktiver Verifikation Aussagen über Algorithmen zu beweisen, die mithilfe der axiomatisch angenommenen Grundalgorithmen aufgebaut werden.
Nachdem Darstellungen für endlichen Mengen und Funktionen eingeführt wurden, werden die Möglichkeiten des Modells an verschiedenen Beispielen aus dem Bereich Differentialgleichungen aufgezeigt. Um praktisch relevante Vektorräume zu beschreiben, werden Sammlungen eingeführt. Diese zunächst rekursiv definierte Klasse von Funktionen erlaubt es, vorhandene Strukturen in Anwendungsproblemen in die mathematische Beschreibung zu übernehmen.
Als Teil des MMATh Projektes dient das Modell dieser Arbeit auch dazu, den zugehörigen MMATh Interpreter zu testen. Definitionen und Sätze werden entsprechend in einer formalen Sprache formuliert. Beweise werden auf hohem Detailgrad ausgeführt, um notwendige Beweisschritte zu identifizieren.
Ein langfristiges Ziel des Projekt ist es, aus formalen mathematischen Texten automatisch verifizierten Code einer beliebigen Programmiersprache zu erzeugen, falls diese Sprache in der Lage ist die axiomatisch geforderten Algorithmen darzustellen. Als erster Schritt wurden hierzu die verifizierten Algorithmen manuell in Scala-Code übersetzt
Durch eine präzise Definition von Darstellungen und Algorithmen können Rechnerobjekte und mathematische Objekte miteinander verbunden werden. Damit wird die Lücke zwischen mathematischer Theorie und Implementierung verringert. Es ist dann möglich, im Sinne von deduktiver Verifikation Aussagen über Algorithmen zu beweisen, die mithilfe der axiomatisch angenommenen Grundalgorithmen aufgebaut werden.
Nachdem Darstellungen für endlichen Mengen und Funktionen eingeführt wurden, werden die Möglichkeiten des Modells an verschiedenen Beispielen aus dem Bereich Differentialgleichungen aufgezeigt. Um praktisch relevante Vektorräume zu beschreiben, werden Sammlungen eingeführt. Diese zunächst rekursiv definierte Klasse von Funktionen erlaubt es, vorhandene Strukturen in Anwendungsproblemen in die mathematische Beschreibung zu übernehmen.
Als Teil des MMATh Projektes dient das Modell dieser Arbeit auch dazu, den zugehörigen MMATh Interpreter zu testen. Definitionen und Sätze werden entsprechend in einer formalen Sprache formuliert. Beweise werden auf hohem Detailgrad ausgeführt, um notwendige Beweisschritte zu identifizieren.
Ein langfristiges Ziel des Projekt ist es, aus formalen mathematischen Texten automatisch verifizierten Code einer beliebigen Programmiersprache zu erzeugen, falls diese Sprache in der Lage ist die axiomatisch geforderten Algorithmen darzustellen. Als erster Schritt wurden hierzu die verifizierten Algorithmen manuell in Scala-Code übersetzt
Subject (DDC)
510 Mathematics
Keywords
Deductive Verification, MMATh, Formal Language, Verified Algorithms, Differential Equations
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690
HÖLLE, Stefan, 2019. Numerical MMATh Verified essential algorithms for solving differential equations [Dissertation]. Konstanz: University of KonstanzBibTex
@phdthesis{Holle2019Numer-48245, year={2019}, title={Numerical MMATh Verified essential algorithms for solving differential equations}, author={Hölle, Stefan}, address={Konstanz}, school={Universität Konstanz} }
RDF
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/48245"> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2020-01-16T14:07:42Z</dcterms:available> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/5/Hoelle_2-wy9t0l1jof5y2.pdf"/> <foaf:homepage rdf:resource="http://localhost:8080/"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/48245"/> <dcterms:title>Numerical MMATh Verified essential algorithms for solving differential equations</dcterms:title> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/39"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2020-01-16T14:07:42Z</dc:date> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/3/Implementation.zip"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/5/Hoelle_2-wy9t0l1jof5y2.pdf"/> <dc:contributor>Hölle, Stefan</dc:contributor> <dc:language>eng</dc:language> <dcterms:issued>2019</dcterms:issued> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/39"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/3/Implementation.zip"/> <dc:creator>Hölle, Stefan</dc:creator> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/6/Hoelle_Langversion_2-wy9t0l1jof5y2.pdf"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/6/Hoelle_Langversion_2-wy9t0l1jof5y2.pdf"/> <dc:rights>terms-of-use</dc:rights> </rdf:Description> </rdf:RDF>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Examination date of dissertation
December 20, 2019
University note
Konstanz, Univ., Doctoral dissertation, 2019
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
Yes