Encoding Monomorphic and Polymorphic Types

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

doi:10.2168/LMCS-2014-1018

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Paper

Encoding Monomorphic and Polymorphic Types

MPS-Authors

/persons/resource/persons183227

Blanchette, Jasmin Christian
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

arXiv:1609.08916.pdf
(Preprint), 790KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Blanchette, J. C., Böhme, S., Popescu, A., & Smallbone, N. (2016). Encoding Monomorphic and Polymorphic Types. doi:10.2168/LMCS-2014-1018.

Cite as: https://hdl.handle.net/11858/00-001M-0000-002B-A954-2

Abstract

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.