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é : Beweisassistenten werden zunehmend in der Formalisierung von Theorien, sowohl in der Informatik als auch in der Mathematik, genutzt. Ihre vielseitigen Logiken mit ausdrucksstarken Typsystemen ermöglichen maschinenkontrollierte Beweise. Dies erhöht die Vertrauenswürdigkeit von komplizierten und detaillierten Beweisen. Im Gegensatz zu Papierbeweisen ist ihr Gebrauch jedoch aufwendiger. Diese Dissertation beschreibt Fortschritte darin, den Abstand zwischen Beweisassistenten höherer Stufe und automatischen Beweissystemen erster Stufe zu schließen, indem automatische Beweissysteme so erweitert werden, dass sie die Möglichkeiten die Beweisassistenten bieten auch bereit stellen. Der erste Beitrag ist die Erweiterung des Superpositionskalküls erster Stufe um ein polymorphes Typsystem, das Typklassen unterstützt. Die Erweiterung beinhaltet einen Beweis der Widerlegungsvollständigkeit. Das Typsystem als Teil des Superpositionskalkül ermöglicht die Übertragung von Problemen aus Beweisassistenten ohne den sonst üblichen Mehraufwand durch Typenenkodierung. Der zweite Beitrag ist die Entwicklung von SupInd, einer Erweiterung von Superposition, die Datentypen und strukturelle Induktion über diese Datentypen erm¨oglicht. SupInd beinhaltet Heuristiken, die die Induktion lenken und Annahmenverst¨arkungstechniken, die auch unabh¨angig des Kalküls benutzt werden können. Die Beiträge wurden im Tool Pirate umgesetzt, die Evaluationen zeigen vielversprechende Ergebnisse.
Document type :
Theses
Complete list of metadatas

Cited literature [66 references]  Display  Hide  Download

https://hal.inria.fr/tel-01592497
Contributor : Stephan Merz <>
Submitted on : Monday, September 25, 2017 - 8:46:32 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Tuesday, December 26, 2017 - 12:56:41 PM

File

thesis_wand.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01592497, version 1

Collections

Citation

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

Share

Metrics

Record views

150

Files downloads

111