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.