Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
Logic Gates and Logical Equivalence of Adders
Shinshu University, Nagano
This is an experimental article which shows that
logical correctness of logic circuits can be easily proven by
the Mizar system. First, we define the notion of logic gates.
Then we prove that an MSB carry of `4 Bit Carry Skip Adder'
is equivalent to an MSB carry of a normal 4 bit adder.
In the last theorem, we show that outputs of the `4 Bit Carry Look
Ahead Adder' are equivalent to the corresponding outputs of the normal
4 bits adder.
The policy here is as follows: when the functional (semantic)
a system is already proven, and the correspondence of the system to a
(normal) logic circuit is given, it is enough to prove the correctness of
circuit if we only prove the logical equivalence between them.
Although the article is very fundamental (it contains
few environment files), it can be applied to real problems.
The key of the method introduced here is to put the specification
of the logic circuit into the Mizar propositional formulae, and to use
the strong inference ability of the Mizar checker. The proof is done
formally so that the automation of the proof writing is possible.
Even in the 5.3.07 version of Mizar, it can handle a formulae of
more than 100 lines, and a formula which contains more than 100 variables.
This means that the Mizar system is enough to prove logical correctness of
middle scaled logic circuits.
Definition of Logical Values and Logic Gates
Logical Equivalence of 4 Bits Adders
Received February 4, 1999
Download a postscript version,
MML identifier index,
Mizar home page]