Skip to main content
SpringerLink
Log in

Ordering constraints on trees

  • Invited Papers
  • Conference paper
  • First Online:
Trees in Algebra and Programming — CAAP'94 (CAAP 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 787))

Included in the following conference series:

Abstract

We survey recent results about ordering constraints on trees and discuss their applications. Our main interest lies in the family of recursive path orderings which enjoy the properties of being total, well-founded and compatible with the tree constructors. The paper includes some new results, in particular the undecidability of the theory of lexicographic path orderings in case of a non-unary signature.

Supported by the Esprit working group CCL, contract EP 6028.

Supported by the Bundesminister für Forschung und Technology, contract ITW 9105, and by the Esprit working group CCL, contract EP 6028. The result Theorem 8 was obtained while the second author visited LRI.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, Lecture Notes in Computer Science, vol. 607, pages 462–476. Springer-Verlag, June 1992.

    Google Scholar 

  2. A. Boudet and H. Comon. About the theory of tree embedding. In M. C. Gaudel and J.-P. Jouannaud, editors, Proc. Int. Joint Conf. on Theory and Practice of Software Development, Lecture Notes in Computer Science, vol. 668, pages 376–390, Orsay, France, Apr. 1993. Springer-Verlag.

    Google Scholar 

  3. A.-C. Caron, J.-L. Coquidé, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, Proc. 5th. Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pages 328–342, Montreal, Canada, 1993. Springer-Verlag.

    Google Scholar 

  4. H. Comon. Equational formulas in order-sorted algebras. In Proc. 17th Int. Coll. on Automata, Languages and Programming, Warwick, Lecture Notes in Computer Science, vol. 443, pages 674–688, Warwick, July 1990. Springer-Verlag.

    Google Scholar 

  5. H. Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387–411, 1990.

    Article  Google Scholar 

  6. H. Comon. Disunification: a survey. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 322–359. MIT Press, 1991.

    Google Scholar 

  7. H. Comon. Constraints in term algebras (short survey). In T. R. M. Nivat, C. Rattray and G. Scollo, editors, Proc. Conf. on Algebraic Methodology and Software Technology, Univ. of Twente, 1993. Springer Verlag, series Workshop in Computing. Invited talk.

    Google Scholar 

  8. H. Comon and R. Treinen. The first-order theory of lexicographic path orderings is undecidable. Research Report RR-93-42, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany, Sept. 1993. Anonymous ftp from duck.dfki.uni-sb.de:/pub/ccl/dfki-saarbruecken.

    Google Scholar 

  9. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, Mar. 1982.

    Article  Google Scholar 

  10. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.

    Google Scholar 

  11. J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. in 14th ICALP Karlsruhe, July 1987.

    Google Scholar 

  12. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rulebased survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 257–321. MIT-Press, 1991.

    Google Scholar 

  13. J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proc. 18th Int. Coll. on Automata, Languages and Programming, Madrid, Lecture Notes in Computer Science, vol. 510, pages 455–468, 1991. Springer-Verlag.

    Google Scholar 

  14. S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Avail-able as a report of the department of computer science, University of Illinois at Urbana-Champaign, 1980.

    Google Scholar 

  15. C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue Française d'Intelligence Artificielle, 4(3):9–52, 1990. Special issue on automatic deduction.

    Google Scholar 

  16. D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.

    Google Scholar 

  17. P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proc. 4th Rewriting Techniques and Applications, Como, Lecture Notes in Computer Science, vol. 488, pages 423–434. Springer-Verlag, Apr. 1991.

    Google Scholar 

  18. R. Nieuwenhuis. Simple LPO constraint solving methods. Inf. Process. Lett., 47:65–69, Aug. 1993.

    Article  Google Scholar 

  19. R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Bruckner, editor, Proc. European Symp. on Programming, Lecture Notes in ComputerScience, vol. 582, pages 371–389, Rennes, 1992. Springer-Verlag.

    Google Scholar 

  20. R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, Lecture Notes in Computer Science, vol. 607, pages 477–491. Springer-Verlag, June 1992.

    Google Scholar 

  21. R. Nieuwenhuis and A. Rubio. A precedence-based total AC-compatible ordering. In C. Kirchner, editor, Proc. 5th Rewriting Techniques and Applications, Montréal, Lecture Notes in Computer Science, vol. 690, pages 374–388. Springer-Verlag, June 1993.

    Google Scholar 

  22. D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182–215, 1985.

    Article  Google Scholar 

  23. W. V. Quine. Concatenation as a basis for arithmetic. Journal of Symbolic Logic, 11(4), 1946.

    Google Scholar 

  24. R. Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437–458, Nov. 1992.

    Article  Google Scholar 

  25. S. Tulipani. Decidability of the existential theory of infinite terms with subterm relation. To appear in Information and Computation, 1994.

    Google Scholar 

  26. K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebras. J. ACM, 34(2):492–510, 1987.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS and LRI, Université de Paris Sud, Bat. 490, F-91405, Orsay cedex, France

    Hubert Comon

  2. German Research Center for Artificial Intelligence (DFKI), Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Ralf Treinen

Authors
  1. Hubert Comon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ralf Treinen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Sophie Tison

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Comon, H., Treinen, R. (1994). Ordering constraints on trees. In: Tison, S. (eds) Trees in Algebra and Programming — CAAP'94. CAAP 1994. Lecture Notes in Computer Science, vol 787. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017470

Download citation

  • DOI: https://doi.org/10.1007/BFb0017470

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57879-6

  • Online ISBN: 978-3-540-48373-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation