Skip to Main content Skip to Navigation

Superposition: Types and Induction

Daniel Wand 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Complete list of metadatas

Cited literature [66 references]  Display  Hide  Download
Contributor : Stephan Merz <>
Submitted on : Monday, September 25, 2017 - 8:46:32 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Tuesday, December 26, 2017 - 12:56:41 PM


Files produced by the author(s)


  • HAL Id : tel-01592497, version 1



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



Record views


Files downloads