Abstract
In a recent paper [BS91] we introduced a new unification algorithm for the combination of disjoint equational theories. Among other consequences we mentioned (1) that the algorithm provides us with a decision procedure for the solvability of general A- and AI-unification problems mad (2) that Kaput and Narendran’s result about the NP decidability of the solvability of general AC- and ACI-unification problems (see [KN91]) may be obtained from our results. In [BS91] we did not give detailled proofs for these two consequences. In the present paper we will treat these problems in more detail. Moreover, we will use the two examples of general A- and AI-unification for a case study of possible optimizations of the basic combination procedure.
Cite
CITATION STYLE
Baader, F., & Schulz, K. U. (1993). General A- and AX-unification via optimized combination procedures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 677 LNCS, pp. 23–42). Springer Verlag. https://doi.org/10.1007/3-540-56730-5_29
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
