Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
Logic Gates and Logical Equivalence of Adders

Yatsuka Nakamura

Shinshu University, Nagano
Summary.

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)
correctness of
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
the new
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.
MML Identifier:
GATE_1

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]