Skip to main content
SpringerLink
Log in
Book cover

International Conference on Constraints in Computational Logics

CCL 1994: Constraints in Computational Logics pp 352–367Cite as

Solving simplification ordering constraints

  • Conference paper
  • First Online:

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

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. H. Comon. Solving Inequations in Term Algebras. International Journal of Foundations of Computer Science 1, pp. 387–411, 1990.

    Google Scholar 

  3. H. Comon and R. Treinen. Ordering Constraints on Trees. In Springer-Verlag LNCS 787, S. Tison, ed., pp. 1–14, 1994.

    Google Scholar 

  4. N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation 3, pp. 69–116, 1987.

    Google Scholar 

  5. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science B, J. van Leeuwen, ed., North-Holland, 1990.

    Google Scholar 

  6. M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with Symbolic Constraints. Revue d'Intelligence Artificielle 4., pp. 9–52, 1990.

    Google Scholar 

  9. R. Nieuwenhuis. Simple LPO Constraint Solving Methods. Information Processing Letters 47, pp. 65–69, 1993.

    Google Scholar 

  10. R. Nieuwenhuis and A. Rubio. Theorem Proving with Ordering Constrained Clauses. In Springer-Verlag LNCS 607, D. Kapur, ed., pp. 477–491, 1992.

    Google Scholar 

  11. D. A. Plaisted. Polynomial Time Termination and Constraint Satisfaction Tests. In Springer-Verlag LNCS 690, C. Kirchner, ed., pp. 405–420, 1993.

    Google Scholar 

  12. R. Treinen. A New Method for Undecidability Proofs for First-order Theories. Journal of Symbolic Computation 14, pp. 437–457, 1992.

    Google Scholar 

  13. K. N. Venkataraman. Decidability of the Purely Existential Fragment of the Theory of Term Algebras. JACM 34, pp. 492–510, 1987.

    Google Scholar 

Download references

Author information

Author notes

  1. Patricia Johann

    Present address: Department of Mathematics and Computer Science, Hobart and William Smith Colleges, 14456, Geneva, NY, USA

  2. Rolf Socher-Ambrosius

    Present address: Fachbereich Elektrotechnik und Informatik, Fachhochschule Ostfriesland, Constantiaplatz 4, D-26723, Emden, Germany

Authors and Affiliations

  1. Fachbereich Informatik, Universität Saarbrücken, D-66123, Saarbrücken, Germany

    Patricia Johann

  2. Max-Planck-Institut für Informatik, D-66123, Saarbrücken, Germany

    Rolf Socher-Ambrosius

Authors
  1. Patricia Johann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rolf Socher-Ambrosius
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Patricia Johann or Rolf Socher-Ambrosius .

Editor information

Jean-Pierre Jouannaud

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation