Abstract
This paper considers the decision problem for the existential fragment of the theory of simplification orderings. A simple, polynomialtime procedure is given for deciding satisfiability of ordering constraints by simplification orderings, and it is also shown that the corresponding problem for total simplification orderings is NP-complete. This latter result can be interpreted as showing that the problem of deciding whether or not a simplification ordering on first-order terms can be linearized is NP-complete.
Supported by the German Ministry for Research and Technology (BMFT) under Grant ITS 9103.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Boudet and H. Comon. About the Theory of Tree Embedding. In Springer-Verlag LNCS 668, M.-C. Gaudel and J.-P. Jouannaud, eds., pp. 376–390, 1993.
H. Comon. Solving Inequations in Term Algebras. International Journal of Foundations of Computer Science 1, pp. 387–411, 1990.
H. Comon and R. Treinen. Ordering Constraints on Trees. In Springer-Verlag LNCS 787, S. Tison, ed., pp. 1–14, 1994.
N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation 3, pp. 69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science B, J. van Leeuwen, ed., North-Holland, 1990.
M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979.
J.-P. Jouannaud and M. Okada. Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable. In Springer-Verlag LNCS 510, J. L. Albert, B. Monien, and M. R. Artalejo, eds., pp. 455–468, 1991.
C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with Symbolic Constraints. Revue d'Intelligence Artificielle 4., pp. 9–52, 1990.
R. Nieuwenhuis. Simple LPO Constraint Solving Methods. Information Processing Letters 47, pp. 65–69, 1993.
R. Nieuwenhuis and A. Rubio. Theorem Proving with Ordering Constrained Clauses. In Springer-Verlag LNCS 607, D. Kapur, ed., pp. 477–491, 1992.
D. A. Plaisted. Polynomial Time Termination and Constraint Satisfaction Tests. In Springer-Verlag LNCS 690, C. Kirchner, ed., pp. 405–420, 1993.
R. Treinen. A New Method for Undecidability Proofs for First-order Theories. Journal of Symbolic Computation 14, pp. 437–457, 1992.
K. N. Venkataraman. Decidability of the Purely Existential Fragment of the Theory of Term Algebras. JACM 34, pp. 492–510, 1987.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johann, P., Socher-Ambrosius, R. (1994). Solving simplification ordering constraints. In: Jouannaud, JP. (eds) Constraints in Computational Logics. CCL 1994. Lecture Notes in Computer Science, vol 845. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0016865
Download citation
DOI: https://doi.org/10.1007/BFb0016865
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58403-2
Online ISBN: 978-3-540-48699-2
eBook Packages: Springer Book Archive