集合合一

能够描述集合的代数中的合一问题已被许多研究者直接或间接地探讨，并在演绎数据库、定理证明、静态分析、快速软件原型设计等各个研究领域找到重要应用。各种提出的解决方案分散在大量文献中。在本文中，我们在集合论层面上形式化地统一阐述了集合合一。我们在抽象层面上解决了解的存在性判定问题。这也提供了对不同类型集合合一问题进行分类的能力。针对每一类问题，统一地提出了合一算法。所呈现的算法部分源自文献——并经过适当的重新审视和分析——部分为新提案。特别地，我们提出了一个用于一般 ACI1 合一的新目标驱动算法，以及一个用于一般 (Ab)(Cl) 合一的新简化算法。