Numerical MMATh Verified essential algorithms for solving differential equations

Hölle, Stefan

Numerical MMATh Verified essential algorithms for solving differential equations

Files

Hoelle_2-wy9t0l1jof5y2.pdf(2.53 MB)

Hoelle_Langversion_2-wy9t0l1jof5y2.pdf(4.14 MB)

Implementation.zip(1.61 MB)

Date

2019

Publication type

Dissertation

Publication status

Published

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

Subject (DDC)

510 Mathematics

Keywords

Deductive Verification, MMATh, Formal Language, Verified Algorithms, Differential Equations

Cite This

ISO 690

HÖLLE, Stefan, 2019. Numerical MMATh Verified essential algorithms for solving differential equations [Dissertation]. Konstanz: University of Konstanz

BibTex

@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>

Examination date of dissertation

December 20, 2019

University note

Konstanz, Univ., Doctoral dissertation, 2019

Bibliography of Konstanz

Yes