Circuit Generated by Terms and Circuit Calculating Terms

Grzegorz Bancerek

University of Bialystok, Shinshu University, Nagano

Summary.

In the paper we investigate the dependence between the structure of circuits and sets of terms. Circuits in our terminology (see [19]) are treated as locally-finite many sorted algebras over special signatures. Such approach enables to formalize every real circuit. The goal of this investigation is to specify circuits by terms and, enentualy, to have methods of formal verification of real circuits. The following notation is introduced in this paper: \begin{itemize} \item structural equivalence of circuits, i.e. equivalence of many sorted signatures, \item embedding of a circuit into another one, \item similarity of circuits (a concept narrower than isomorphism of many sorted algebras over equivalent signatures), \item calculation of terms by a circuit according to an algebra, \item specification of circuits by terms and an algebra. \end{itemize}

MML Identifier: CIRCTRM1

Contents (PDF format)

1. Circuit Structure Generated by Terms
2. Circuit Generated by Terms
3. Correctness of a Term Circuit
4. Circuit Similarity
5. Term Specification

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Introduction to trees. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[4] Grzegorz Bancerek. K\"onig's Lemma. Journal of Formalized Mathematics, 3, 1991.

[5] Grzegorz Bancerek. Sets and functions of trees and joining operations of trees. Journal of Formalized Mathematics, 4, 1992.

[6] Grzegorz Bancerek. Joining of decorated trees. Journal of Formalized Mathematics, 5, 1993.

[7] Grzegorz Bancerek. Subtrees. Journal of Formalized Mathematics, 6, 1994.

[8] Grzegorz Bancerek. Terms over many sorted universal algebra. Journal of Formalized Mathematics, 6, 1994.

[9] Grzegorz Bancerek. Minimal signature for partial algebra. Journal of Formalized Mathematics, 7, 1995.

[10] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[11] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Journal of Formalized Mathematics, 7, 1995.

[12] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[13] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[14] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[15] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[16] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[17] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[18] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.

[19] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, I. Journal of Formalized Mathematics, 6, 1994.

[20] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.

[21] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Journal of Formalized Mathematics, 6, 1994.

[22] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Journal of Formalized Mathematics, 7, 1995.

[23] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[24] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[25] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.

[26] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[27] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[28] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[29] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.