Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Logical Equivalence of Formulae


Oleg Okhotnikov
Ural University, Ekaterinburg

This work has been done while the author visited Warsaw University in Bia{\l}ystok, in winter 1994--1995.

MML Identifier: CQC_THE3

The terminology and notation used in this paper have been introduced in the following articles [8] [9] [7] [1] [3] [2] [6] [4] [5]

Contents (PDF format)

Acknowledgments

The author wishes to thank Professor A. Trybulec for many helpful talks during the preparation of this paper.

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.
[5] Agata Darmochwal. A first-order predicate calculus. Journal of Formalized Mathematics, 2, 1990.
[6] Piotr Rudnicki and Andrzej Trybulec. A first order language. Journal of Formalized Mathematics, 1, 1989.
[7] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[8] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[9] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received January 24, 1995

[ Download a postscript version, MML identifier index, Mizar home page]