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

lmcs:2628 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 4
Encoding Monomorphic and Polymorphic Types

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

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.


Source : oai:arXiv.org:1609.08916
DOI : 10.2168/LMCS-12(4:13)2016
Volume: Volume 12, Issue 4
Published on: April 27, 2017
Submitted on: May 14, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 262 times.
This article's PDF has been downloaded 107 times.