Automated Deduction and Computational Complexity

这个项目研究了方程匹配和统一的几个不同的计算方面，重点是交换半群的方程理论AC及其推广。调查以三管齐下的计划进行。首先，对方程统一中的计数问题的研究将试图确定计算以方程理论为模的最小完全统一子数的确切复杂性。这个计数问题比相应的决策问题更准确地反映了方程统一的计算困难；而且，当只考虑决策问题时，它带来了方程匹配和统一之间的某些被掩盖的差异。在研究的第二部分中，将系统地研究等式统一中的有效列表算法；这些算法应该列举两个给定项的所有极小完全一致，但也应该满足某些期望的性能保证，例如列出任意两个连续一致的合理有界的延迟。这一领域的进展可能会导致发现新的统一算法，并开发出比较这些算法的严格方法。最后，将对联想-交换匹配问题进行实验研究，主要目的是识别此类问题的硬随机实例，并可能揭示联想-交换匹配中的阈值或相变现象。这项研究还可能为匹配和统一算法的实验评估提供新的基准。

This project investigates several different computational aspects of equational matching and unification with emphasis on the equational theory AC of commutative semigroups and its extensions. The investigation is carried out in a three-pronged plan. First, a study of counting problems in equational unification will attempt to identify the exact complexity of computing the number of minimal complete unifiers modulo an equational theory. This counting problem reflects more accurately the computational difficulties of equational unification than the corresponding decision problem does; moreover, it brings out certain differences between equational matching and unification that are masked, when only decision problems are considered. In the second part of the Investigation will be a systematic investigation of efficient listing algorithms in equational unification; these algorithms should enumerate all minimal complete unifiers of two given terms, but should also satisfy certain desirable performance guarantees, such as a reasonably bounded delay in listing any two consecutive unifiers. Progress in the area may lead to the discovery of novel unification algorithms and to the development of a rigorous methodology for comparing such algorithms. Finally, there will be an experimental investigation of associative-commutative matching problems; the main aim is to identify hard random instances of such problems and possibly to unveil threshold or phase-transition phenomena in associative- commutative matching. This investigation may also produce new benchmarks for the experimental evaluation of matching and unification algorithms.