Abstract
We show that unification in certain extensions of shallow equational theories is decidable. Our extensions generalize the known classes of shallow or standard equational theories. In order to prove decidability of unification in the extensions, a class of Horn clause sets called sorted shallow equational theories is introduced. This class is a natural extension of tree automata with equality constraints between brother subterms as well as shallow sort theories. We show that saturation under sorted superposition is effective on sorted shallow equational theories. So called semi-linear equational theories can be effectively transformed into equivalent sorted shallow equational theories and generalize the classes of shallow and standard equational theories.
This work was partially supported by the CONSOLE project.
This work was supported by the German science foundation program Deduktion.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Ganzinger, H., Lynch, C. & Snyder, W. (1995), ‘Basic paramodulation', Information and Computation 121(2), 172–192.
Bogaert, B. & Tison, S. (1992), Equality and disequality constraints on direct subterms in tree automata, in A. Finkel & M. Jantzen, eds, ‘Proceedings of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92', Vol. 577 of LNCS, Springer, pp. 161–171.
Comon, H. (1995), Sequentially, second order monadic logic and tree automata, in ‘Proceedings 10th IEEE Symposium on Logic in Computer Science, LICS'95', IEEE Computer Society Press, pp. 508–517.
Comon, H., Haberstrau, M. & Jouannaud, J.-P. (1994), ‘Syntacticness, cyclesyntacticness and shallow theories', Information and Computation 111(1), 154–191.
Dershowitz, N. & Jouannaud, J.-P. (1990), Rewrite systems, in J. van Leeuwen, ed., ‘Handbook of Theoretical Computer Science', Vol. B, Elsevier Science Publishers, chapter 6, pp. 243–320.
Durand, I. & Middeldorp, A. (1997), Decidable call by need computations in term rewriting (extended abstract), in W. McCune, ed., ‘Automated Deduction — CADE-14, 14th International Conference on Automated Deduction', LNCS 1249, Springer-Verlag, Townsville, North Queensland, Australia, pp. 4–18.
Fassbender, H. & Maneth, S. (1996), A strict border for the decidability of e-unification for recursive functions, in M. Hanus & M. Rodríguez-Artalejo, eds, ‘Algebraic and Logic Programming (ALP-5):5th international conference, Aachen, Germany, September 25–27, 1996', Vol. 1139 of Lecture notes in computer science, Springer, Berlin.
Ganzinger, H., Meyer, C. & Weidenbach, C. (1997), Soft typing for ordered resolution, in ‘Proceedings of the 14th International Conference on Automated Deduction, CADE-14', Vol. 1249 of LNAI, Springer, Townsville, Australia, pp. 321–335.
Jacquemard, F. (1996), Decidable approximations of term rewriting systems, in H. Ganzinger, ed., ‘Rewriting Techniques and Applications, 7th International Conference, RTA-96', Vol. 1103 of LNCS, Springer, pp. 362–376.
Jacquemard, F., Meyer, C. & Weidenbach, C. (1998), Unification in extensions of shallow equational theories, MPI-Report MPI-I-98-2-002, Max-Planck-Institut für Informatik, Saarbrücken, Germany.
Kaji, Y., Toru, F. & Kasami, T. (1997), ‘Solving a unification problem under constrained substitutions using tree automata', Journal of Symbolic Computation 23, 79–117.
Kirchner, C. (1986), Computing unification algorithms, in ‘Proceedings of the First Symposium on Logic in Computer Science', Cambridge, Massachusetts, pp. 206–216.
Limet, S. & Réty, P. (1997), E-unification by means of tree tuple synchronized grammars, in M. Bidoit & M. Dauchet, eds, ‘TAPSOFT '97: Proceedings of the Seventh Joint Conference on Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France', Vol. 1214, Springer-Verlag, Lille, France.
Nieuwenhuis, R. (1996), Basic paramodulation and decidable theories (extended abstract), in ‘Proceedings 11th IEEE Symposium on Logic in Computer Science, LICS'96', IEEE Computer Society Press, pp. 473–482.
Nieuwenhuis, R. & Rubio, A. (1995), ‘Theorem proving with ordering and equality constrained clauses', Journal of Symbolic Computation 19, 321–351.
Otto, F., Narendran, P. & Dougherty, D. J. (1995), Some independence results for equational unification, in J. Hsiang, ed., ‘Rewriting Techniques and Applications, 6th International Conference, RTA-95', LNCS 914, Springer-Verlag, Kaiserslautern, Germany, pp. 367–381.
Oyamaguchi, M. (1990), ‘On the word problem for right-ground term-rewriting systems', The Transactions of the IEICE 73(5), 718–723.
Weidenbach, C. (1997), ‘Spass version 0.49', Journal of Automated Reasoning 18(2), 247–252.
Weidenbach, C. (1998), Sorted unification and tree automata, in W. Bibel & P. H. Schmitt, eds, ‘Automated Deduction, A Basis for Applications', Vol. 1, Kluwer, chapter 2.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Jacquemard, F., Meyer, C., Weidenbach, C. (1998). Unification in extensions of shallow equational theories. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052362
Download citation
DOI: https://doi.org/10.1007/BFb0052362
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive