Handling Polymorphism in Automated Deduction
Handling Polymorphism in Automated Deduction
复制标题
处理自动推导中的多态性
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Stéphane Lescuyer
中科院分区：
文献类型：
--
作者：
Jean;Stéphane Lescuyer
多态性已经成为一种通过从特定类型的定义中抽象出泛型定义来设计简短且可重用的程序的常用方法。这种方便在逻辑中也是有价值的，因为它减轻了说明符编写逻辑符号的冗余声明的负担。然而，顶级的自动定理证明器，如XNUMX，Yices或其他SMT-LIB不处理多态性。为此，我们提出了有效的减少多态性在未排序和许多排序的一阶逻辑。对于每一个编码，我们表明，公式和它们的编码对应的自动定理证明的上下文中是逻辑上等价的。效率的基调是尽可能少地干扰证明者，特别是用于特殊排序的内部决策过程，例如整数线性算术，我们对其进行特殊处理。相应的实现在Why/Caduceus工具包的框架中给出。
Polymorphism has become a common way of designing short and reusable programs by abstracting generic definitions from type-specific ones. Such a convenience is valuable in logic as well, because it unburdens the specifier from writing redundant declarations of logical symbols. However, top shelf automated theorem provers such as Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To this end, we present efficient reductions of polymorphism in both unsorted and many-sorted first order logics. For each encoding, we show that the formulas and their encoded counterparts are logically equivalent in the context of automated theorem proving. The efficiency keynote is to disturb the prover as little as possible, especially the internal decision procedures used for special sorts, e.g. integer linear arithmetic, to which we apply a special treatment. The corresponding implementations are presented in the framework of the Why/Caduceus toolkit.