Automated Deduction and Computational Complexity

点击翻译按钮获取中文摘要

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.