Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 DetailsÜbersicht
  Superposition: Types and Induction

Wand, D. (2017). Superposition: Types and Induction. PhD Thesis, Universität des Saarlandes, Saarbrücken.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-002D-E99C-5 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-002D-FBC8-7
Genre: Hochschulschrift

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
http://scidok.sulb.uni-saarland.de/volltexte/2017/6952/ (beliebiger Volltext)
Beschreibung:
-
OA-Status:
Grün
externe Referenz:
http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de (Verlagsvertrag)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

einblenden:
ausblenden:
 Urheber:
Wand, Daniel1, 2, Autor           
Weidenbach, Christoph1, Ratgeber           
Blanchette, Jasmin Christian1, Gutachter           
Sutcliffe, Geoff1, Gutachter           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs. However, they incur a significant overhead compared to pen-and-paper proofs. This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants. My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants. My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus. I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2017-08-042017-09-142017
 Publikationsstatus: Erschienen
 Seiten: x, 167 p.
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: wandphd2017
URN: urn:nbn:de:bsz:291-scidok-69522
 Art des Abschluß: Doktorarbeit

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: