The Knuth-Bendix Completion Algorithm and Its Specification in Z

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 memorandum 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. Great Britain. (rrh)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1989
Accession Number
ADA216298

Entities

People

  • A. Smith

Organizations

  • Royal Signals and Radar Establishment

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Automatic
  • Computers
  • Construction
  • Copyrights
  • Demographic Cohorts
  • Equations
  • Executives
  • Identities
  • Intellectual Property
  • Language
  • Literature
  • Mathematics
  • Sequences
  • Specifications

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Artificial Intelligence
  • Criminal Law