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

Introducing Euclidean Relations to Mizar

,

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

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

Full text

Abstract. In this paper we present the methodology of implementing a new enhancement of the Mizar proof checker based on enabling special processing of Euclidean predicates, i.e. binary predicates which fulfill a specific variant of transitivity postulated by Euclid. Typically, every proof step in formal mathematical reasoning is associated with a formula to be proved and a list of references used to justify the formula. With the proposed enhancement, the Euclidean property of given relations can be registered during their definition, and so the verification of some proof steps related to these relations can be automated to avoid explicit referencing.

References

  1. A. Trybulec, “Mizar,” in The Seventeen Provers of the World, ser. Lecture Notes in Computer Science, F. Wiedijk, Ed., vol. 3600. Berlin, Heidelberg: Springer-Verlag, 2006, pp. 20–23. [Online]. Available: http://dx.doi.org/10.1007/11542384_4
  2. G. Bancerek, C. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, K. Pąk, and J. Urban, “Mizar: State-of-the-art and beyond,” in Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings, ser. Lecture Notes in Computer Science, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, Eds., vol. 9150. Springer, 2015, pp. 261–279. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-20615-8_17
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. Euclid, The Elements, books I-XIII. New York: Barnes & Noble, 2006.
  17. A. Naumowicz, “Enhanced processing of adjectives in Mizar,” in Computer Reconstruction of the Body of Mathematics, ser. Studies in Logic, Grammar and Rhetoric, A. Grabowski and A. Naumowicz, Eds. University of Białystok, 2009, vol. 18(31), pp. 89–101.
  18. 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
  19. A. Naumowicz and R. Piliszek, “Accessing the Mizar library with a weakly strict Mizar parser,” 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. 77–82. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-42547-4_6
  20. J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, P. Rudnicki, and J. Urban, “Licensing the Mizar Mathematical Library,” in Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics, ser. MKM’11, Lecture Notes in Computer Science, J. H. Davenport, W. M. Farmer, J. Urban, and F. Rabe, Eds., vol. 6824. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 149–163. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-22673-1_11
  21. 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, ser. Lecture Notes in Computer Science, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton, Eds., vol. 6167. Springer, 2010, pp. 300–314. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-14128-7_26
  22. G. Bancerek, “Tarski’s classes and ranks,” Formalized Mathematics, vol. 1, no. 3, pp. 563–567, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-3/classes1.pdf
  23. M. Muzalewski, “Midpoint algebras,” Formalized Mathematics, vol. 1, no. 3, pp. 483–488, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-3/midsp_1.pdf
  24. E. Kusak, W. Leończuk, and M. Muzalewski, “Parallelity spaces,” Formalized Mathematics, vol. 1, no. 2, pp. 343–348, 1990. [Online]. Available: http://fm.mizar.org/1990-1/pdf1-2/parsp_1.pdf
  25. M. Kohlhase, M. Johansson, B. R. Miller, L. de Moura, and F. W. Tompa, Eds., Intelligent Computer Mathematics – 9th International Conference, CICM 2016, Bialystok, Poland, July 25–29, 2016, Proceedings, ser. Lecture Notes in Computer Science, vol. 9791. Springer, 2016. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-42547-4
  26. 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