Algebraic Approach to Algorithmic Logic

Grzegorz Bancerek

Formalized Mathematics (2014)

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

Abstract

top
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.

How to cite

top

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

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.