A comparison of the variable-abstraction and constant-abstraction methods for associative-commutative unification

The constant-abstraction and variable-abstraction methods for associative-commutative unification were proposed by Herold, Livesey, and Siekmann and by Stickel, respectively. These methods are compared here for efficiency and conceptual purity. The pure variable-abstraction method is easier to implement but less efficient for the variables and constants case than the constant-abstraction method. With obvious refinements, the former method can be made comparably efficient and similar in behavior to the latter. The refined method uses solutions of homogeneous linear Diophantine equations under additional constraints, instead of the conceptually simpler homogeneous or inhomogeneous linear Diophantine equations without additional constraints of the pure variable-abstraction method or the constant-abstraction method.This paper resulted from a visit to the University of Kaiserslautern, during which discussions with Alexander Herold and Jörg Siekmann enabled each of us to gain a greater understanding and appreciation of one another's algorithms. The visit was partially supported by the Deutsche Forschungsgemeinschaft, Sonderforschungsbereich 314, Künstliche Intelligenz-Wissensbasierte Systeme. Preparation of this paper was supported, in part, by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Space and Naval Warfare Systems Command. The views and conclusions contained herein are those of the author and should not be interpreted as representative of the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States government. Approved for public release. Distribution unlimited.     

Hilbert's tenth problem is of unification type zero

We show that the problem of finding integer solutions to a polynomial equation over the integers has unification type zero, i.e. there exist polynomial equations which have unifiers, but which have no minimal and complete set of unifiers: In particular, it is shown that the equation uv=w+z has no minimal and complete set of solutions.     

Computational Complexity of Simultaneous Elementary Matching Problems

The simultaneous elementary E-matching problem for an equational theory E is to decide whether there is an E-matcher for a given system of equations in which the only nonconstant function symbols occurring in the terms to be matched are the ones constrained by the equational axioms of E. We study the computational complexity of simultaneous elementary matching problems for the equational theories A of semigroups, AC of commutative semigroups, and ACU of commutative monoids. In each case, we delineate the boundary between NP-completeness and solvability in polynomial time by considering two parameters, the number of equations in the systems and the number of constant symbols in the signature. Moreover, we analyze further the intractable cases of simultaneous elementary AC-matching and ACU-matching by also taking into account the maximum number of occurrences of each variable. Using combinatorial optimization techniques, we show that if each variable is restricted to having at most two occurrences, then several cases of simultaneous elementary AC-matching and ACU-matching can be solved in polynomial time.     

A note on the complexity of matching patterns with variables

A word matches a pattern with variables (i.e., a string that contains terminal symbols and variable symbols) if and only if it can be obtained from the pattern by substituting the variables by terminal words. To decide for a given word whether or not it matches a pattern with variables is an NP-complete problem, which has been independently discovered and investigated in different areas of theoretical computer science and which has applications in various contexts. In this work, we show that the problem of matching patterns with variables remains NP-complete even if every variable has at most two occurrences. In addition to this, we show that if patterns can be represented as special kinds of planar graphs, then they can be matched in polynomial time.     

一个复杂度为max(O(|C||U|),O(|C|2|U/C|))的快速属性约简算法

以基数排序的思想设计了一个新的求U／C的算法,其时间复杂度被降为O（｜C｜｜U｜）．经研究发现,以近似质量作为启发信息并非十分理想,故以快速缩小搜索空间为目的设计了一个新的较为合理的度量属性重要性的计算公式,并给出了该公式的递归计算公式．计算该公式的算法复杂度被降低到O（｜C-P｜｜U＇-Up＇｜）．用新公式作为启发信息,设计了一个时间复杂度为max（o（O（｜C｜｜U｜）,O（｜C^2｜U／C｜））的快速属性约简算法,并用一个实例说明了算法．实验结果表明新算法不仅具有高效性而且能处理大型决策表．