@MISC{REWRITE1.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Reduction Relations},
  SECTION1 = {Forgetting concatenation and reduction sequence},
  SECTION2 = {Reducibility, convertibility and normal forms},
  SECTION3 = {Terminating reductions},
  SECTION4 = {Church-Rosser property},
  SECTION5 = {Completion method},
  DAY = {14},
  MONTH = {November},
  YEAR = {1995},
  ADDRESS1 = {Institute of Mathematics\\Polish Academy of Sciences},
  SUMMARY = {The goal of the article is to start the formalization
of Knuth-Bendix completion method (see \cite{BachmairDershowitz},
     \cite{KlopMiddeldorp} or \cite{HofLinCS};
     see also \cite{KnuthBendix},\cite{Huet81}),
i.e. to formalize the concept of the completion
of a reduction relation.
The completion of a reduction relation $R$ is
a complete reduction relation equivalent to $R$ such that
convertible elements have the same normal forms.
The theory formalized in the article includes concepts and facts
concerning normal forms, terminating reductions, Church-Rosser property,
and equivalence of reduction relations.}}

