Skip to main content
SpringerLink
Log in

The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

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

Abstract

We show that the first-order theory of any Knuth-Bendix order in the case of the signatures consisting of unary function symbols and constants is decidable. Our decision procedure uses interpretation of unary terms as trees and uses decidability of the weak monadic second-order theory of binary trees. One area of applications of our result is automated deduction, since using the first-order theory of the Knuth-Bendix orders we can decide an important class of ordering constraints. umaiy uccs.

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 T. Nipkow. Term Rewriting and and All That. Cambridge University press, Cambridge, 1998.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  3. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tom-masi. Tree automata techniques and applications. Available on:http://www.grappa.univ-lille3.fr/tata, 1997.

  4. H. Comon and R. Treinen. The first-order theory of lexicographic path orderings is undecid-able. Theoretical Computer Science, 176(1–2):67–87, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  5. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

    Article  MATH  MathSciNet  Google Scholar 

  6. Yuri Ershov. Problems of decidability and constructive models. Nauka, 1980. (in Russian).

    Google Scholar 

  7. W. Hodges. Model theory. Cambridge University Press, 1993.

    Google Scholar 

  8. J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the sub-term property is decidable. In Automata, Languages and Programming, 18th International Colloquium (ICALP), volume 510 of Lecture Notes in Computer Science, pages 455–468, 1991.

    Google Scholar 

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

    Google Scholar 

  10. K. Korovin and A. Voronkov. A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In Proc. 15th Annual IEEE Symp. on Logic in Computer Science, pages 291–302, Santa Barbara, California, June 2000.

    Google Scholar 

  11. K. Korovin and A. Voronkov. Knuth-bendix ordering constraint solving is NP-complete. In F. Orejas, P.G. Spirakis, and J. van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, volume 2076 of Lecture Notes in Computer Science, pages 979–992. Springer Verlag, 2001.

    Google Scholar 

  12. K. Korovin and A. Voronkov. Verifying orientability of rewrite rules using the Knuth-Bendix order. In A. Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, volume 2051 of Lecture Notes in Computer Science, pages 137–153. Springer Verlag, 2001.

    Google Scholar 

  13. M. Maher. Complete axiomatizations of the algebras of finite, rational and infi nite trees. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 348–357, 1988.

    Google Scholar 

  14. Narendran and Rusinowitch. The theory of total unary rpo is decidable. In First International Conference on Computational Logic, volume 1861 of Lecture Notes in Computer Science, pages 660–672, 2000.

    Google Scholar 

  15. Narendran, Rusinowitch, and Verma. RPO constraint solving is in NP. In CSL: 12thWorkshop on Computer Science Logic, volume 1584, pages 385–398. LNCS, Springer-Verlag, 1998.

    Google Scholar 

  16. R. Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65–69, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  17. R. Nieuwenhuis and J.M. Rivero. Solved forms for path ordering constraints. In In Proc. 10th International Conference on Rewriting Techniques and Applications (RTA), volume 1631 of Lecture Notes in Computer Science, pages 1–15, Trento, Italy, 1999.

    Google Scholar 

  18. Michael O. Rabin. Decidable theories. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.3, pages 595–629. North-Holland, Amsterdam, 1977.

    Google Scholar 

  19. James W. Thatcher and Jesse B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2( 1): 57–81,1968.

    Article  MathSciNet  Google Scholar 

  20. Ralf Treinen. A new method for undecidability proofs of first order theories. In Foundations of Software Technology and Theoretical Computer Science,(FSTTCS), 10th conference, volume 472 of Lecture Notes in Computer Science, pages 48–62, 1990. (journal version [21]).

    Google Scholar 

  21. Ralf Treinen. A new method for undecidablity proofs of first order theories. Journal of Symbolic Computations, 14(5):437–458, 1992.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, Manchester

    Konstantin Korovin & Andrei Voronkov

Authors
  1. Konstantin Korovin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Korovin, K., Voronkov, A. (2002). The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation