Superposition: Types and Induction

Résumé : 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.
Type de document :
Thèse
Computer Science [cs]. Saarland University, 2017. English
Liste complète des métadonnées

Littérature citée [66 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01592497
Contributeur : Stephan Merz <>
Soumis le : lundi 25 septembre 2017 - 08:46:32
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02
Document(s) archivé(s) le : mardi 26 décembre 2017 - 12:56:41

Fichier

thesis_wand.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-01592497, version 1

Citation

Daniel Wand. Superposition: Types and Induction. Computer Science [cs]. Saarland University, 2017. English. 〈tel-01592497〉

Partager

Métriques

Consultations de la notice

98

Téléchargements de fichiers

56