规范重写与模 Shostak 理论的基 AC 完成：设计与实现
计算机科学中的逻辑
2015-07-01 v2
摘要
AC-完成能有效处理模结合交换函数符号的等式。当输入为基项时，该过程终止并为字问题提供判定算法。本文提出了一种基 AC-完成的模块化扩展，用于判定等式理论、用户定义的 AC 符号、未解释符号以及任意签名不相交的 Shostak 理论 X 的组合中的公式。我们的算法称为 AC(X)，通过将理论 X 现有的规范器和求解器以模块化方式增强基 AC-完成而获得。这种集成依赖于规范重写，这是一种类似于规范化重写的新关系，它将规范器整合到重写步骤中。证明了 AC(X) 的可靠性、完备性和终止性，并已实现以扩展 Alt-Ergo 定理证明器的核心。
引用
@article{arxiv.1207.3262,
title = {Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation},
author = {Sylvain Conchon and Evelyne Contejean and Mohamed Iguernelala},
journal= {arXiv preprint arXiv:1207.3262},
year = {2015}
}
备注
30 pages, full version of the paper TACAS'11 paper "Canonized Rewriting and Ground AC-Completion Modulo Shostak Theories" accepted for publication by LMCS (Logical Methods in Computer Science)