# Encoding Monomorphic and Polymorphic Types

arXiv: https://arxiv.org/abs/1609.08916 · HTML: https://mlsanity.com/paper/1609.08916/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2016.

## Built on by (most cited first, 2 of 2)

- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Superposition with Lambdas](https://mlsanity.com/paper/2102.00453/) (2021)

## Abstract (arXiv)

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.