Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 11

Proceedings of the 2017 Federated Conference on Computer Science and Information Systems

Formalization of the Algebra of Nominative Data in Mizar

, , ,

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 ()

Full text

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

  1. 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.
  2. 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.
  3. E. Lee and S. Seshia, Introduction to embedded systems: A cyberphysical systems approach. Lulu.com, 2013.
  4. J. Sifakis, “Rigorous design of cyber-physical systems,” in Embedded Computer Systems (SAMOS), 2012 International Conference on. IEEE, 2012, pp. 319–319.
  5. D. Liberzon, Switching in Systems and Control (Systems & Control: Foundations & Applications). Birkhauser Boston Inc., 2003.
  6. R. Goebel, R. G. Sanfelice, and A. Teel, “Hybrid dynamical systems,” Control Systems, IEEE, vol. 29, no. 2, pp. 28–93, 2009.
  7. H. Nielson and F. Nielson, Semantics with applications – a formal introduction, ser. Wiley professional computing. Wiley, 1992.
  8. R. Floyd, “Assigning meanings to programs,” Mathematical aspects of computer science, vol. 19, no. 19–32, 1967.
  9. C. Hoare, “An axiomatic basis for computer programming,” Commun. ACM, vol. 12, no. 10, pp. 576–580, 1969.
  10. 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.
  11. J. Ball, “Finite time blow-up in nonlinear problems,” Nonlinear Evolution Equations, pp. 189–205, 1978.
  12. 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
  13. H. A. Levine, “The role of critical exponents in blowup theorems,” Siam Review, vol. 32, no. 2, pp. 262–288, 1990.
  14. A. Goriely, Integrability and nonintegrability of dynamical systems. World Scientific Publishing Company, 2001, vol. 19.
  15. 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.
  16. 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.
  17. 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
  18. 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.
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. N. S. Nikitchenko, “A composition nominative approach to program semantics,” IT-TR 1998-020, Technical University of Denmark, Tech. Rep., 1998.
  38. M. Nikitchenko and S. Shkilniak, Mathematical logic and theory of algorithms. Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (in Ukrainian), 2008.
  39. 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.
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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