集合统一
Set Unification
摘要：
能够描述集合的代数中的统一问题已经被许多研究人员直接或间接地解决，并且在各种研究领域中找到了重要的应用-例如，演绎数据库、定理证明、静态分析、快速软件原型。所提出的各种解决方案分布在大量文献中。在本文中，我们提供了一个统一的介绍，统一的集合，形式化它在集合论的水平。我们解决的问题，决定存在的解决方案在一个抽象的水平。这也提供了对不同类型的集合统一问题进行分类的能力。统一算法统一提出解决统一问题，在每个这样的类。所提出的算法部分来自文献-并适当地重新审视和分析-和部分新颖的建议。特别是，我们提出了一个新的目标驱动的算法一般ACI 1统一和一个新的简单的算法一般（Ab）（Cl）统一。
英文摘要：
The unification problem in algebras capable of describing sets has been tackled, directly or indirectly, by many researchers and it finds important applications in various research areas--e.g., deductive databases, theorem proving, static analysis, rapid software prototyping. The various solutions proposed are spread across a large literature. In this paper we provide a uniform presentation of unification of sets, formalizing it at the level of set theory. We address the problem of deciding existence of solutions at an abstract level. This provides also the ability to classify different types of set unification problems. Unification algorithms are uniformly proposed to solve the unification problem in each of such classes. The algorithms presented are partly drawn from the literature--and properly revisited and analyzed--and partly novel proposals. In particular, we present a new goal-driven algorithm for general ACI1 unification and a new simpler algorithm for general (Ab)(Cl) unification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
