Publikation: Numerical MMATh Verified essential algorithms for solving differential equations
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Sammlungen
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
Zusammenfassung in einer weiteren Sprache
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
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
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>
