Hierarchical Combination

Serdar Erbatur⁵, Deepak Kapur¹, Andrew M. Marshall², Paliath Narendran³, and Christophe Ringeissen⁴

¹University of New Mexico, USA

²Naval Research Laboratory, USA

³University at Albany, SUNY, USA

⁴LORIA – INRIA Nancy-Grand Est, France

⁵Dipartimento di Informatica, Università degli Studi di Verona, Italy

Abstract. A novel approach is described for the combination of unification algorithms for two equational theories E₁ and E₂ 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”.

LNAI 7898, p. 249 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013