Skip to main content
SpringerLink
Log in

On equality up-to constraints over finite trees, context unification, and one-step rewriting

  • Conference paper
  • First Online:
Automated Deduction—CADE-14 (CADE 1997)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1249))

Included in the following conference series:

Abstract

We introduce equality up-to constraints over finite trees and investigate their expressiveness. Equality up-to constraints subsume equality constraints, subtree constraints, and one-step rewriting constraints. We establish a close correspondence between equality up-to constraints over finite trees and context unification. Context unification subsumes string unification and is subsumed by linear second-order unification. We obtain the following three new results. The satisfiability problem of equality up-to constraints is equivalent to context unification, which is an open problem. The positive existential fragment of the theory of one-step rewriting is decidable. The ∃*∀*∃* fragment of the theory of context unification is undecidable.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Baader and K. Schulz. Unification in the union of disjoint equational theories. Int. Conferece on Automated Deduction, volume 607 of LNCS, pages 50–65. 1992.

    Google Scholar 

  2. F. Baader and J. Siekmann. Handbook of Logic in Artificial Intelligence and Logic Programming, chapter Unification Theory. Oxford University Press, 1993.

    Google Scholar 

  3. A. Caron, J.-L. Coquide, and M. Dauchet. Encompassment properties and automata with constraints. Int. Conference on Rewriting Techniques and Applications, volume 690 of LNCS, pages 328–342. 1993.

    Google Scholar 

  4. H. Comon. Completion of rewrite systems with membership constraints. Int. Coll. on Automata, Languages and Programming, volume 623 of LNCS, 1992.

    Google Scholar 

  5. M. Dalrymple, S. Shieber, and F. Pereira. Ellipsis and higher order unification. Linguistics and Philosophy, 14:399–452, 1991.

    Article  Google Scholar 

  6. C. Gardent, and M. Kohlhase. Higher-order coloured unification and natural language semantics. Annual meeting of the ACL, 1996.

    Google Scholar 

  7. W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.

    Article  MathSciNet  Google Scholar 

  8. G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Article  MathSciNet  Google Scholar 

  9. J. Jaffar. Minimal and complete word unification. J. of the ACM, 37(1):47–85, 1990.

    Article  MathSciNet  Google Scholar 

  10. A. Kościelski and L. Pacholski. Complexity of makanin's algorithm. Journal of the ACM, 43(4), 1996.

    Google Scholar 

  11. A. Lentin and M. Schützenberger. A combinatorial problem in the theory of free monoids. Conference on Combinatorical Mathematics and its Applications, 1969.

    Google Scholar 

  12. J. Lévy. Linear second order unification. Int. Conference on Rewriting Techniques and Applications, number 1103 of LNCS, 1996.

    Google Scholar 

  13. G. Makanin. The problem of solvability of equations in a free semigroup. Soviet Akad. Nauk SSSR, 223(2), 1977.

    Google Scholar 

  14. J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. Int. Conference on Rewriting Techniques and Applications, LNCS. 1997.

    Google Scholar 

  15. A. Markov. The theory of algorithms. Trudy Mat. Inst. Steklov, 1(42), 1954. English Translation in Israel Program for Scientific Translations, Jerusalem, 1968.

    Google Scholar 

  16. J. Niehren, M. Pinkal, and P. Ruhrberg. A uniform approach to underspecification and parallelism, 1997. Submitted. Available from http://www.ps.unisb.de/~niehren.

    Google Scholar 

  17. J. Niehren, M. Pinkal, and P. Ruhrberg. On equality up-to constraints over finite trees, context unification, and one-step rewriting. Full version. Available from http://www.ps.uni-sb.de/~niehren.

    Google Scholar 

  18. J. Pécuchet. Solution principale et rang d'un system d'èquations avec constantes dans le monoïde libre. Discrete Mathematics, 48:253–274, 1984.

    Article  MathSciNet  Google Scholar 

  19. T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333–364, 1973.

    Article  MathSciNet  Google Scholar 

  20. M. Pinkal. Radical underspecification. CLAUS Report 72, Universität des Saarlandes, 1996.

    Google Scholar 

  21. G. D. Plotkin. Building in equational theories. Machine Intelligence, (7):73–90, 1972.

    Google Scholar 

  22. M. Schmidt-Schauß. Unification of stratified second-order terms. Internal report 12/94, J. W. Goethe Universität, Frankfurt, Germany, 1994.

    Google Scholar 

  23. K. U. Schulz. Word unification and transformation of generalized equations. J. of Automated Reasoning, 11:149–184, 1993.

    Article  MathSciNet  Google Scholar 

  24. J. H. Siekmann. String-unification: Part 1. Internal Report CSM7, Essex University, 1975.

    Google Scholar 

  25. R. Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14:437–457, 1992.

    Article  MathSciNet  Google Scholar 

  26. R. Treinen. The first-order theory of one-step rewriting is undecidable. Int. Conf. on Rewriting Techniques and Appl., number 1103 of LNCS, pages 276–286, 1996.

    Google Scholar 

  27. S. Tulipani. Decidability of the existential theory of infinite terms with subterm relation. Journal on Information and Computation, 103(2), 1993.

    Google Scholar 

  28. K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebra. Journal of the ACM, 34(2):492–510, Apr. 1987.

    Article  MathSciNet  Google Scholar 

  29. S. Vorobyov. The first-order theory of one step rewriting in linear noetherian systems is undecidable. Int. Conf. on Rewriting Techn. and Appl., LNCS. 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Systems Lab, Germany

    Joachim Niehren

  2. Department of Computational Linguistics, Universität des Saarlandes, Saarbrücken, Germany

    Manfred Pinkal & Peter Ruhrberg

Authors
  1. Joachim Niehren
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manfred Pinkal
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Ruhrberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

William McCune

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Niehren, J., Pinkal, M., Ruhrberg, P. (1997). On equality up-to constraints over finite trees, context unification, and one-step rewriting. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-63104-6_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63104-0

  • Online ISBN: 978-3-540-69140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation