Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995
Association of Mizar Users
Reduction Relations
-
Grzegorz Bancerek
-
Institute of Mathematics, Polish Academy of Sciences
Summary.
-
The goal of the article is to start the formalization
of Knuth-Bendix completion method (see [2],
[10] or [1];
see also [11],[9]),
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.
The terminology and notation used in this paper have been
introduced in the following articles
[12]
[15]
[14]
[3]
[6]
[16]
[4]
[5]
[13]
[7]
[8]
-
Forgetting concatenation and reduction sequence
-
Reducibility, convertibility and normal forms
-
Terminating reductions
-
Church-Rosser property
-
Completion method
Bibliography
- [1]
S. Abramsky, D. M. Gabbay, and S. E. Maibaum, editors.
\em Handbook of Logic in Computer Science, vol. 2: Computational
structures.
Clarendon Press, Oxford, 1992.
- [2]
Leo Bachmair and Nachum Dershowitz.
Critical pair criteria for completion.
\em Journal of Symbolic Computation, 6(1):1--18, 1988.
- [3]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
- [4]
Grzegorz Bancerek.
The well ordering relations.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
- [6]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [7]
Czeslaw Bylinski.
Some properties of restrictions of finite sequences.
Journal of Formalized Mathematics,
7, 1995.
- [8]
Patricia L. Carlson and Grzegorz Bancerek.
Context-free grammar --- part I.
Journal of Formalized Mathematics,
4, 1992.
- [9]
Gerard Huet.
A complete proof of correctness of the Knuth-Bendix completion.
\em Journal of Computer and System Sciences, 23(1):3--57, 1981.
- [10]
Jan Willem Klop and Aart Middeldorp.
An introduction to Knuth-Bendix completion.
\em CWI Quarterly, 1(3):31--52, 1988.
- [11]
Donald E. Knuth and Peter B. Bendix.
Simple word problems in universal algebras.
In J. Leech, editor, \em Computational Problems in Abstract
Algebras, pages 263--297, Oxford, 1970. Pergamon.
- [12]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [13]
Andrzej Trybulec.
Many-sorted sets.
Journal of Formalized Mathematics,
5, 1993.
- [14]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
- [15]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [16]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received November 14, 1995
[
Download a postscript version,
MML identifier index,
Mizar home page]