## Introducing Euclidean Relations to Mizar

### Adam Naumowicz, Artur Kornilowicz

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

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

- 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
- 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
- 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
- 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. 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
- 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, “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. 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
- Euclid, The Elements, books I-XIII. New York: Barnes & Noble, 2006.
- 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.
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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