Skip to main content
SpringerLink
Log in
Book cover

Z User Workshop pp 195–220Cite as

The Knuth-Bendix Completion Algorithm and Its Specification in Z

  • Conference paper

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

Proving that something is a consequence of a set of axioms can be very difficult. The Knuth-Bendix completion algorithm attempts to automate this process when the axioms are equations. The algorithm is bound up in the area of term rewriting, and so this paper contains an introduction to the theory of term rewriting, followed by an overview of the algorithm. Finally a formal specification of the algorithm is given using the language Z [7, 8].

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. D. Bramson “Tools for the Specification, Design, Analysis and Verification of software”. RSRE report number 87005 (1987)

    Google Scholar 

  2. N. Dershowitz “Termination of Rewriting” pp 69–115 in Journal of Symbolic Computation, Vol 3 (1987)

    Google Scholar 

  3. A. J. J. Dick “Automated Equational Reasoning and the Knuth-Bendix Algorithm: An Informal Introduction” Rutherford Appleton Laboratory report number RAL-88–043 (1988)

    Google Scholar 

  4. D.E. Knuth and P.B. Bendix “Simple Word Problems in Universal Algebras” pp 263–297 in Computational Problems in Abstract Algebra, ed J. Leech, Pergamon press (1970)

    Google Scholar 

  5. MALPAS Intermediate Language (Version 4.0). Rex, Thompson and partners (1987)

    Google Scholar 

  6. J. A. Robinson “A Machine-Oriented Logic Based on the Resolution Principle” pp 23–41 in Journal of the Association for Computing Machinery, Vol 12, No 1 (1965)

    Google Scholar 

  7. C. T. Sennett “Review of Type Checking and Scope Rules of the Specification Language Z”. RSRE report number 87017 (1987)

    Google Scholar 

  8. J. M. Spivey “The Z Notation: A Reference Manual” Prentice-Hall International, Series in Computing Science (1988)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RSRE Malvern, RSRE, St Andrews Rd, Great Malvern, Worcs, WR14 3PS, UK

    Alf Smith

Authors
  1. Alf Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Oxford University Programming Research Group, 8-11 Keble Road, Oxford, UK

    John E. Nicholls MA

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag London

About this paper

Cite this paper

Smith, A. (1990). The Knuth-Bendix Completion Algorithm and Its Specification in Z. In: Nicholls, J.E. (eds) Z User Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3877-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3877-8_14

  • Publisher Name: Springer, London

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

  • Online ISBN: 978-1-4471-3877-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation