Abstract
In this part the properties of unification of uninterpreted order-sorted terms are investigated and rule-based unification algorithms are presented. We show that for elementary, regular signatures Σ-unification is decidable and finitary. In the general case when we have signatures with term declarations, unification is undecidable and infinitary. We also determine the unification behaviour under certain restrictions such as linearity.
Throughout this part we assume that the given signature Σ is finite.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(1989). Unification of uninterpreted sorted terms. In: Schmidt-Schauß, M. (eds) Computational Aspects of an Order-Sorted Logic with Term Declarations. Lecture Notes in Computer Science, vol 395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024069
Download citation
DOI: https://doi.org/10.1007/BFb0024069
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51705-4
Online ISBN: 978-3-540-46774-8
eBook Packages: Springer Book Archive