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.
@article{bwmeta1.element.doi-10_2478_forma-2014-0025,
author = {Grzegorz Bancerek},
title = {Algebraic Approach to Algorithmic Logic},
journal = {Formalized Mathematics},
volume = {22},
year = {2014},
pages = {225-255},
zbl = {1311.03057},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0025}
}
Grzegorz Bancerek. Algebraic Approach to Algorithmic Logic. Formalized Mathematics, Tome 22 (2014) pp. 225-255. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2014-0025/
[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] | Zbl 06213852
[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. | Zbl 06213858
[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. | Zbl 0915.03002
[25] Grazyna Mirkowska and Andrzej Salwicki. Algorithmic Logic. PWN-Polish Scientific Publisher, 1987. | Zbl 1159.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.