Abstract
A novel approach is described for the combination of unification algorithms for two equational theories E1 and E2 which share function symbols. We are able to identify a set of restrictions and a combination method such that if the restrictions are satisfied the method produces a unification algorithm for the union of non-disjoint equational theories. Furthermore, we identify a class of theories satisfying the restrictions. The critical characteristics of the class is the hierarchical organization and the shared symbols being restricted to "inner constructors". © 2013 Springer-Verlag.
Cite
CITATION STYLE
Erbatur, S., Kapur, D., Marshall, A. M., Narendran, P., & Ringeissen, C. (2013). Hierarchical combination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7898 LNAI, pp. 249–266). https://doi.org/10.1007/978-3-642-38574-2_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
