# Algebraic Approach to Algorithmic Logic

Formalized Mathematics (2014)

- Volume: 22, Issue: 3, page 225-255
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topGrzegorz Bancerek. "Algebraic Approach to Algorithmic Logic." Formalized Mathematics 22.3 (2014): 225-255. <http://eudml.org/doc/270902>.

@article{GrzegorzBancerek2014,

abstract = {We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and theory are defined. Propositional calculus and quantifier calculus with equality are explored according to [24]. A language is introduced with language signature including free variables, substitution, and equality. Algorithmic logic requires a bialgebra structure which is an extension of language signature and program algebra. While-if algebra of generator set and algebraic signature is bialgebra with appropriate properties and is used as basic type of algebraic logic.},

author = {Grzegorz Bancerek},

journal = {Formalized Mathematics},

keywords = {propsitional calcus; quantifier calcus; algorithmic logic},

language = {eng},

number = {3},

pages = {225-255},

title = {Algebraic Approach to Algorithmic Logic},

url = {http://eudml.org/doc/270902},

volume = {22},

year = {2014},

}

TY - JOUR

AU - Grzegorz Bancerek

TI - Algebraic Approach to Algorithmic Logic

JO - Formalized Mathematics

PY - 2014

VL - 22

IS - 3

SP - 225

EP - 255

AB - We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and theory are defined. Propositional calculus and quantifier calculus with equality are explored according to [24]. A language is introduced with language signature including free variables, substitution, and equality. Algorithmic logic requires a bialgebra structure which is an extension of language signature and program algebra. While-if algebra of generator set and algebraic signature is bialgebra with appropriate properties and is used as basic type of algebraic logic.

LA - eng

KW - propsitional calcus; quantifier calcus; algorithmic logic

UR - http://eudml.org/doc/270902

ER -

## References

top- [1] Grzegorz Bancerek. Mizar analysis of algorithms: Preliminaries. Formalized Mathematics, 15(3):87-110, 2007. doi:10.2478/v10037-007-0011-x.[Crossref]
- [2] Grzegorz Bancerek. Program algebra over an algebra. Formalized Mathematics, 20(4): 309-341, 2012. doi:10.2478/v10037-012-0037-6.[Crossref] Zbl06213852
- [3] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
- [4] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.
- [5] Grzegorz Bancerek. Algebra of morphisms. Formalized Mathematics, 6(2):303-310, 1997.
- [6] Grzegorz Bancerek. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997.
- [7] Grzegorz Bancerek. Translations, endomorphisms, and stable equational theories. Formalized Mathematics, 5(4):553-564, 1996.
- [8] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
- [9] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
- [10] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281-290, 1990.
- [11] Grzegorz Bancerek. Ordinal arithmetics. Formalized Mathematics, 1(3):515-519, 1990.
- [12] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
- [13] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485-492, 1996.
- [14] Ewa Burakowska. Subalgebras of the universal algebra. Lattices of subalgebras. Formalized Mathematics, 4(1):23-27, 1993.
- [15] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
- [16] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.
- [17] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
- [18] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [19] Czesław Bylinski. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521-527, 1990.
- [20] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
- [21] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [22] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
- [23] Jarosław Kotowicz, Beata Madras, and Małgorzata Korolkiewicz. Basic notation of universal algebra. Formalized Mathematics, 3(2):251-253, 1992.
- [24] Elliott Mendelson. Introduction to Mathematical Logic. Chapman Hall/CRC, 1997. http://books.google.pl/books?id=ZO1p4QGspoYC. Zbl0915.03002
- [25] Grazyna Mirkowska and Andrzej Salwicki. Algorithmic Logic. PWN-Polish Scientific Publisher, 1987. Zbl1159.68360
- [26] Beata Perkowska. Free universal algebra construction. Formalized Mathematics, 4(1): 115-120, 1993.
- [27] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1): 67-74, 1996.
- [28] Krzysztof Retel. Properties of first and second order cutting of binary relations. Formalized Mathematics, 13(3):361-365, 2005.
- [29] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.
- [30] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990.
- [31] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37-42, 1996.
- [32] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993.
- [33] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- [34] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990.
- [35] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.