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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
F. Baader and J. Siekmann. Handbook of Logic in Artificial Intelligence and Logic Programming, chapter Unification Theory. Oxford University Press, 1993.
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.
H. Comon. Completion of rewrite systems with membership constraints. Int. Coll. on Automata, Languages and Programming, volume 623 of LNCS, 1992.
M. Dalrymple, S. Shieber, and F. Pereira. Ellipsis and higher order unification. Linguistics and Philosophy, 14:399–452, 1991.
C. Gardent, and M. Kohlhase. Higher-order coloured unification and natural language semantics. Annual meeting of the ACL, 1996.
W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.
G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
J. Jaffar. Minimal and complete word unification. J. of the ACM, 37(1):47–85, 1990.
A. Kościelski and L. Pacholski. Complexity of makanin's algorithm. Journal of the ACM, 43(4), 1996.
A. Lentin and M. Schützenberger. A combinatorial problem in the theory of free monoids. Conference on Combinatorical Mathematics and its Applications, 1969.
J. Lévy. Linear second order unification. Int. Conference on Rewriting Techniques and Applications, number 1103 of LNCS, 1996.
G. Makanin. The problem of solvability of equations in a free semigroup. Soviet Akad. Nauk SSSR, 223(2), 1977.
J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. Int. Conference on Rewriting Techniques and Applications, LNCS. 1997.
A. Markov. The theory of algorithms. Trudy Mat. Inst. Steklov, 1(42), 1954. English Translation in Israel Program for Scientific Translations, Jerusalem, 1968.
J. Niehren, M. Pinkal, and P. Ruhrberg. A uniform approach to underspecification and parallelism, 1997. Submitted. Available from http://www.ps.unisb.de/~niehren.
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.
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.
T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333–364, 1973.
M. Pinkal. Radical underspecification. CLAUS Report 72, Universität des Saarlandes, 1996.
G. D. Plotkin. Building in equational theories. Machine Intelligence, (7):73–90, 1972.
M. Schmidt-Schauß. Unification of stratified second-order terms. Internal report 12/94, J. W. Goethe Universität, Frankfurt, Germany, 1994.
K. U. Schulz. Word unification and transformation of generalized equations. J. of Automated Reasoning, 11:149–184, 1993.
J. H. Siekmann. String-unification: Part 1. Internal Report CSM7, Essex University, 1975.
R. Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14:437–457, 1992.
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.
S. Tulipani. Decidability of the existential theory of infinite terms with subterm relation. Journal on Information and Computation, 103(2), 1993.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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