Abstract
In this paper the decidability of unification in pseudo-linear sort theories is shown. In contrast to standard unification, variables range over subsets of the domain described by sorts. The denotations of sorts are fixed by declarations in a sort theory. Then two terms are unifiable, if they are unifiable in the standard sense and the assignments of the unifier satisfy the restrictions on the domain variables with respect to the sort theory. This problem is known to be undecidable in general, but is known to be decidable for elementary, weak-elementary, linear and semi-linear sort theories. So-called pseudo-linear sort theories properly include all these sort theories. We show that the problem of whether two terms are unifiable with respect to a pseudo-linear sort theory is decidable and of unification type infinitary.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bruno Bogaert and Sophie Tison. Equality and disequality constraints on direct subterms in tree automata. In A. Finkel and M. Jantzen, editors, Proc. of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92, volume 577 of LNCS, pages 161–171. Springer, 1992.
Anne-Cécile Caron, Hubert Comon, Jean-Luc Coquidé, Max Dauchet, and Florent Jacquemard. Pumping, cleaning and symbolic constraints solving. In Serge Abiteboul and Eli Shamir, editors, Automata Languages and Programming. 21st International Colloquium, ICALP'94, volume 820 of LNCS, pages 436–447. Springer, 1994.
Hubert Comon. Inductive proofs by specification transformations. In Rewriting Techniques and Applications, RTA-89, volume 355 of LNCS, pages 76–91. Springer, 1989.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243–320. Elsevier Science Publishers, 1990.
Alan M. Frisch and Anthony G. Cohn. An abstract view of sorted unification. In 11th International Conference on Automated Deduction, CADE-11, LNCS 607, volume 607 of LNCS, pages 178–192. Springer, 1992.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.L. Lassez and G. Plotkin, editors, Computational Logic, Essays in Honor of Alan Robinson, chapter 8, pages 257–321. MIT Press, 1991.
Manfred Schmidt-Schauß. Computational aspects of an order sorted logic with term declarations, volume 395 of LNAI. Springer, 1989.
Jörg Siekmann. Unification theory. Journal of Symbolic Computation, Special Issue on Unification, 7:207–274, 1989.
Tomás E. Uribe. Sorted unification using set constraints. In 11th International Conference on Automated Deduction, CADE-11, volume 607 of LNCS, pages 163–177. Springer, 1992.
Christoph Walther. Unification in many-sorted theories. In Proceedings of the 6th ECAI, pages 383–392. North-Holland, 1983.
Christoph Weidenbach. Unification in sort theories and its applications. Annals of Mathematics and Artificial Intelligence. To appear.
Christoph Weidenbach. Extending the resolution method with sorts. In Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93, pages 60–65. Morgan Kaufmann, 1993.
Christoph Weidenbach. First-order tableaux with sorts. Journal of the Interest Group in Pure and Applied Logics, IGPL, 3(6):887–906, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weidenbach, C. (1996). Unification in pseudo-linear sort theories is decidable. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_99
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_99
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive