一句话：系统研究并实现将单态与多态类型编码到无类型一阶逻辑的方案，提升自动定理证明效率且保持可靠完备。
许多自动定理证明器只支持无类型逻辑，而现有从带类型逻辑到无类型一阶逻辑的翻译要么臃肿，要么不可靠。本文系统地把单调性方法用于去除编码中的冗余，并形式化分析多种编码，使其在保持可靠性与完备性的同时提高效率。作者将方法扩展到 rank-1 多态，提出基于“cover”这一新概念的多态符号翻译方案。新编码已作为 Isabelle/HOL 的 Sledgehammer 工具的一部分实现，文中给出可靠性与正确性的非形式证明，并在 Isabelle/HOL 中形式化了单态部分。评估表明新编码远优于先前方案。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BlanchetteBPS13,
title = {Encoding Monomorphic and Polymorphic Types},
author = {Jasmin Christian Blanchette and Sascha Böhme and Andrei Popescu and Nicholas Smallbone},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:13)2016}
}