Canonical Forms and Unification.

Abstract

Fay has described a complete T-unification for equational theories T that possess a complete set of reductions as defined by Knuth and Bendix. This algorithm relies essentially on using the narrowing process defined by Lankford. In this paper it is first studied the relations between narrowing and unification and it gives a new version of Fay's algorithm. It then shows how to eliminate many redundancies in this algorithm and gives a sufficient condition for its termination. Finally it is shown how to extend the previous results to various kinds of canonical term rewriting systems.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1980
Accession Number
ADA087640

Entities

People

  • Jean-marie Hullot

Organizations

  • SRI International

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • Artificial Intelligence
  • Classification
  • Computer Science
  • Computers
  • Equations
  • Formal Languages
  • Mathematics
  • Notation
  • Observers
  • Redundancy
  • Security
  • Sequences
  • Theoretical Computer Science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Linguistics