Jasmin Christian Blanchette ; Sascha Böhme ; Andrei Popescu ; Nicholas Smallbone - Encoding Monomorphic and Polymorphic Types

lmcs:2628 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 4 - https://doi.org/10.2168/LMCS-12(4:13)2016
Encoding Monomorphic and Polymorphic Types

Authors: Jasmin Christian Blanchette ; Sascha Böhme ; Andrei Popescu ; Nicholas Smallbone

    Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.

    Volume: Volume 12, Issue 4
    Published on: April 27, 2017
    Accepted on: January 2, 2017
    Submitted on: May 14, 2014
    Keywords: Computer Science - Logic in Computer Science

    Linked publications - datasets - softwares

    Source : ScholeXplorer IsCitedBy ARXIV 2205.01981
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.itp.2022.16
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2205.01981
    • 10.4230/lipics.itp.2022.16
    • 10.48550/arxiv.2205.01981
    • 2205.01981
    The Isabelle ENIGMA
    Goertzel, Zarathustra A. ; Jakubův, Jan ; Kaliszyk, Cezary ; Olšák, Miroslav ; Piepenbrock, Jelle ; Urban, Josef ;

    6 Documents citing this article

    Consultation statistics

    This page has been seen 1068 times.
    This article's PDF has been downloaded 361 times.