## Formalization of the Algebra of Nominative Data in Mizar

### Artur Korniłowicz, Andrii Kryvolap, Mykola Nikitchenko, Ievgen Ivanov

DOI: http://dx.doi.org/10.15439/2017F301

Citation: Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 11, pages 237–244 (2017)

Abstract. In the paper we describe a formalization of the notion of a nominative data with simple names and complex values in the Mizar proof assistant. Such data can be considered as a partial variable assignment which allows arbitrarily deep nesting and can be useful for formalizing semantics of programs that operate in real time environment and/or process complex data structures and for reasoning about the behavior of such programs.

### References

- T. Hoare. (2004) The verifying compiler: A grand challenge for computing research. Gresham College, 18/03/2004, Barnard’s Inn Hall. http://www.cs.ox.ac.uk/files/6187/Grand.pdf.
- J. Shi, J. Wan, H. Yan, and H. Suo, “A survey of cyber-physical systems,” in Wireless Communications and Signal Processing (WCSP). IEEE, 2011, pp. 1–6.
- E. Lee and S. Seshia, Introduction to embedded systems: A cyberphysical systems approach. Lulu.com, 2013.
- J. Sifakis, “Rigorous design of cyber-physical systems,” in Embedded Computer Systems (SAMOS), 2012 International Conference on. IEEE, 2012, pp. 319–319.
- D. Liberzon, Switching in Systems and Control (Systems & Control: Foundations & Applications). Birkhauser Boston Inc., 2003.
- R. Goebel, R. G. Sanfelice, and A. Teel, “Hybrid dynamical systems,” Control Systems, IEEE, vol. 29, no. 2, pp. 28–93, 2009.
- H. Nielson and F. Nielson, Semantics with applications – a formal introduction, ser. Wiley professional computing. Wiley, 1992.
- R. Floyd, “Assigning meanings to programs,” Mathematical aspects of computer science, vol. 19, no. 19–32, 1967.
- C. Hoare, “An axiomatic basis for computer programming,” Commun. ACM, vol. 12, no. 10, pp. 576–580, 1969.
- A. Korniłowicz, A. Kryvolap, M. Nikitchenko, and I. Ivanov, “An approach to formalization of an extension of Floyd-Hoare logic.” Accepted for publication in Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2017), 15-18 May 2017, Kyiv, Ukraine, 2017.
- J. Ball, “Finite time blow-up in nonlinear problems,” Nonlinear Evolution Equations, pp. 189–205, 1978.
- Y. Zhou, Z. Yang, H. Zhang, and Y. Wang, “Theoretical analysis for blow-up behaviors of differential equations with piecewise constant arguments,” Appl. Math. Comput., vol. 274, no. C, pp. 353–361, Feb. 2016. [Online]. Available: http://dx.doi.org/10.1016/j.amc.2015.10.080
- H. A. Levine, “The role of critical exponents in blowup theorems,” Siam Review, vol. 32, no. 2, pp. 262–288, 1990.
- A. Goriely, Integrability and nonintegrability of dynamical systems. World Scientific Publishing Company, 2001, vol. 19.
- V. Skobelev, M. Nikitchenko, and I. Ivanov, “On algebraic properties of nominative data and functions,” in Information and Communication Technologies in Education, Research, and Industrial Applications, ser. Communications in Computer and Information Science, V. Ermolayev, H. Mayr, M. Nikitchenko, A. Spivakovsky, and G. Zholtkevych, Eds. Springer International Publishing, 2014, vol. 469, pp. 117–138.
- F. Wiedijk, “The seventeen provers of the world. Foreword by Dana S. Scott.” ser. Lecture Notes in Artificial Intelligence, F. Wiedijk, Ed. Springer-Verlag Berlin Heidelberg, 2006, vol. 3600.
- A. Grabowski, A. Korniłowicz, and A. Naumowicz, “Four decades of Mizar,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 191–198, October 2015. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9345-1
- G. Bancerek, C. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, K. Pa̧k, and J. Urban, “Mizar: State-of-the-art and beyond,” ser. Lecture Notes in Computer Science. Springer, 2015, vol. 9150, pp. 261–279.
- A. Naumowicz, “Interfacing external CA systems for Gröbner bases computation in Mizar proof checking,” International Journal of Computer Mathematics, vol. 87, no. 1, pp. 1–11, January 2010. [Online]. Available: http://dx.doi.org/10.1080/00207160701864459
- A. Naumowicz, “SAT-enhanced Mizar proof checking,” in Intelligent Computer Mathematics – International Conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings, ser. Lecture Notes in Computer Science, S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, Eds., vol. 8543. Springer, 2014, pp. 449–452. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-08434-3_37
- A. Naumowicz, “Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 285–294, October 2015. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9332-6
- A. Korniłowicz, “On rewriting rules in Mizar,” Journal of Automated Reasoning, vol. 50, no. 2, pp. 203–210, February 2013. [Online]. Available: http://dx.doi.org/10.1007/s10817-012-9261-6
- A. Korniłowicz, “Flexary connectives in Mizar,” Computer Languages, Systems & Structures, vol. 44, pp. 238–250, December 2015. [Online]. Available: http://dx.doi.org/10.1016/j.cl.2015.07.002
- A. Korniłowicz, “Definitional expansions in Mizar,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 257–268, October 2015. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9331-7
- G. Nelson and D. C. Oppen, “Fast decision procedures based on congruence closure,” J. ACM, vol. 27, pp. 356–364, April 1980. [Online]. Available: http://doi.acm.org/10.1145/322186.322198
- A. Grabowski, A. Korniłowicz, and C. Schwarzweller, “Equality in computer proof-assistants,” in Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, ser. Annals of Computer Science and Information Systems, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., vol. 5. IEEE, 2015, pp. 45–54. [Online]. Available: http://dx.doi.org/10.15439/2015F229
- A. Naumowicz and C. Byliński, “Improving Mizar texts with properties and requirements,” in Mathematical Knowledge Management, Third International Conference, MKM 2004 Proceedings, ser. MKM’04, Lecture Notes in Computer Science, A. Asperti, G. Bancerek, and A. Trybulec, Eds., vol. 3119, 2004, pp. 290–301. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-27818-4_21
- A. Korniłowicz, “Enhancement of Mizar texts with transitivity property of predicates,” in Intelligent Computer Mathematics – 9th International Conference, CICM 2016, Bialystok, Poland, July 25–29, 2016, Proceedings, ser. Lecture Notes in Computer Science, M. Kohlhase, M. Johansson, B. R. Miller, L. de Moura, and F. W. Tompa, Eds., vol. 9791. Springer, 2016, pp. 157–162. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-42547-4_12
- A. Trybulec, “Tarski Grothendieck set theory,” Formalized Mathematics, vol. 1, no. 1, pp. 9–11, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf
- A. Grabowski, “Mechanizing complemented lattices within Mizar type system,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 211–221, October 2015. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9333-5
- A. Grabowski, A. Korniłowicz, and C. Schwarzweller, “On algebraic hierarchies in mathematical repository of Mizar,” in Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, ser. Annals of Computer Science and Information Systems, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., vol. 8. IEEE, 2016, pp. 363–371. [Online]. Available: http: //dx.doi.org/10.15439/2016F520
- A. Grabowski and M. Jastrzębska, “Rough set theory from a math-assistant perspective,” in Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings, ser. Lecture Notes in Computer Science, M. Kryszkiewicz, J. F. Peters, H. Rybinski, and A. Skowron, Eds., vol. 4585. Springer, 2007, pp. 152–161. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-73451-2_17
- K. Pąk, “Improving legibility of natural deduction proofs is not trivial,” Logical Methods in Computer Science, vol. 10, no. 3, pp. 1–30, 2014. [Online]. Available: http://dx.doi.org/10.2168/LMCS-10(3:23)2014
- K. Pąk, “Automated improving of proof legibility in the Mizar system,” in Intelligent Computer Mathematics – International Conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings, ser. Lecture Notes in Computer Science, S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, Eds., vol. 8543. Springer, 2014, pp. 373–387. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-08434-3_27
- K. Pąk, “Improving legibility of formal proofs based on the close reference principle is NP-hard,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 295–306, October 2015. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9337-1
- A. Grabowski and C. Schwarzweller, “On duplication in mathematical repositories,” in Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5–10, 2010. Proceedings, 2010, pp. 300–314. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-14128-7_26
- N. S. Nikitchenko, “A composition nominative approach to program semantics,” IT-TR 1998-020, Technical University of Denmark, Tech. Rep., 1998.
- M. Nikitchenko and S. Shkilniak, Mathematical logic and theory of algorithms. Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (in Ukrainian), 2008.
- A. Grabowski, A. Korniłowicz, and A. Naumowicz, “Mizar in a nutshell,” Journal of Formalized Reasoning, Special Issue: User Tutorials I, vol. 3, no. 2, pp. 153–245, December 2010.
- C. Byliński, “Partial functions,” Formalized Mathematics, vol. 1, no. 2, pp. 357–367, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-2/partfun1.pdf
- G. Bancerek and K. Hryniewiecki, “Segments of natural numbers and finite sequences,” Formalized Mathematics, vol. 1, no. 1, pp. 107–114, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-1/finseq_1. pdf
- C. Byliński, “Functions and their basic properties,” Formalized Mathematics, vol. 1, no. 1, pp. 55–65, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-1/funct_1.pdf
- E. Woronowicz, “Relations and their basic properties,” Formalized Mathematics, vol. 1, no. 1, pp. 73–83, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-1/relat_1.pdf
- G. Bancerek, “König’s theorem,” Formalized Mathematics, vol. 1, no. 3, pp. 589–593, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-3/card_3.pdf
- A. Trybulec, “Binary operations applied to functions,” Formalized Mathematics, vol. 1, no. 2, pp. 329–334, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-2/funcop_1.pdf
- C. Byliński, “The modification of a function by a function and the iteration of the composition of a function,” Formalized Mathematics, vol. 1, no. 3, pp. 521–527, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-3/funct_4.pdf
- C. Byliński, “Some basic properties of sets,” Formalized Mathematics, vol. 1, no. 1, pp. 47–53, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-1/zfmisc_1.pdf
- S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, Eds., Intelligent Computer Mathematics – International Conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings, ser. Lecture Notes in Computer Science, vol. 8543. Springer, 2014. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-08434-3