The Experts below are selected from a list of 85347 Experts worldwide ranked by ideXlab platform

Coghetto Roland - One of the best experts on this subject based on the ideXlab platform.

  • Cross-Ratio in Real Vector Space
    DeGruyter Open, 2019
    Co-Authors: Coghetto Roland
    Abstract:

    Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]).It is also equivalent to the notion of “Mesure algèbrique”1, to the opposite of the notion of Teilverhältnis2 or to the opposite of the ordered length-ratio [9].In the second part, we introduce the classic notion of “cross-ratio” of 4 points aligned in a real vector space.Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion3 [9]:The cross-ratio of a quadruple of distinct points on the real line with coordinates x1, x2, x3, x4 is given by:(x1,x2;x3,x4)=x3-x1x3-x2.x4-x2x4-x1In the Mizar Mathematical Library, the vector spaces were first defined by Kusak, Leonczuk and Muzalewski in the article [6], while the actual real vector space was defined by Trybulec [10] and the complex vector space was defined by Endou [4]. Nakasho and Shidama have developed a solution to explore the notions introduced by different authors4 [7]. The definitions can be directly linked in the HTMLized version of the Mizar library5.The study of the cross-ratio will continue within the framework of the Klein- Beltrami model [2], [3]. For a generalized cross-ratio, see Papadopoulos [8].Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21–32, 2018. doi:10.2478/forma-2018-0003.Roland Coghetto. Klein-Beltrami model. Part II. Formalized Mathematics, 26(1):33–48, 2018. doi:10.2478/forma-2018-0004.Noboru Endou. Complex linear space and complex normed space. Formalized Mathematics, 12(2):93–102, 2004.Jadwiga Knop. About a certain generalization of the affine ratio of three points and unharmonic ratio of four points. Bulletin of the Section of Logic, 32(1–2):33–42, 2003.Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.Kazuhisa Nakasho and Yasunari Shidama. Documentation generator focusing on symbols for the HTML-ized Mizar library. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, CICM 2015, volume 9150 of Lecture Notes in Computer Science, pages 343–347. Springer, Cham, 2015. doi:10.1007/978-3-319-20615-8_25.Athanase Papadopoulos and Sumio Yamada. On the projective geometry of constant curvature spaces. Sophus Lie and Felix Klein: The Erlangen Program and Its Impact in Mathematics and Physics, 23:237–245, 2015.Jürgen Richter-Gebert. Perspectives on projective geometry: a guided tour through real and complex geometry. Springer Science & Business Media, 2011.Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.271476

  • Tarski Geometry Axioms. Part IV – Right Angle
    DeGruyter Open, 2019
    Co-Authors: Coghetto Roland, Grabowski Adam
    Abstract:

    In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).Roland Coghetto - Rue de la Brasserie 5, 7100 La Louvi`ere, BelgiumAdam Grabowski - Institute of Informatics, University of Białystok, PolandGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.Michael Beeson and Larry Wos. OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning, volume 8562 of Lecture Notes in Computer Science, pages 495–510. Springer, 2014. doi:10.1007/978-3-319-08587-6 38.Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, Jan 2019. doi:10.1007/s10472-018-9606-x.Pierre Boutry, Gabriel Braun, and Julien Narboux. Formalization of the Arithmetization of Euclidean Plane Geometry and Applications. Journal of Symbolic Computation, 90: 149–168, 2019. doi:10.1016/j.jsc.2018.04.007.Pierre Boutry, Charly Gries, Julien Narboux, and Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, 62(1):1–68, 2019.Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289–313, 2017. doi:10.1515/forma-2017-0028.Sana Stojanovic Durdevic, Julien Narboux, and Predrag Janičić. Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249–269, 2015.Adam Grabowski. Tarski’s geometry modelled in Mizar Computerized proof assistant. In Maria Ganzha, Leszek Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of ACSIS – Annals of Computer Science and Information Systems, pages 373–381, 2016. doi:10.15439/2016F290.Adam Grabowski and Roland Coghetto. Tarski’s geometry and the Euclidean plane in Mizar. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Białystok, Poland, July 25–29, 2016, volume 1785 of CEUR-WS, pages 4–9, 2016.Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In Francisco Botana and Tomas Recio, editors, Automated Deduction in Geometry, pages 139–156, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. ISBN 978-3-540-77356-6.William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167–176, 2014. doi:10.2478/forma-2014-0017.Wolfram Schwabhcuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.271758

  • Klein-Beltrami Model. Part II
    DeGruyter Open, 2018
    Co-Authors: Coghetto Roland
    Abstract:

    Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2, 3, 15, 4]. With the Mizar system [1], [10] we use some ideas are taken from Tim Makarios’ MSc thesis [12] for formalized some definitions (like the tangent) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as a further development of Tarski’s geometry in the formal setting [9].Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Eugenio Beltrami. Saggio di interpetrazione della geometria non-euclidea. Giornale di Matematiche, 6:284–322, 1868.Eugenio Beltrami. Essai d’interprétation de la géométrie non-euclidéenne. In Annales scientifiques de l’École Normale Supérieure. Trad. par J. Hoüel, volume 6, pages 251–288. Elsevier, 1869.Karol Borsuk and Wanda Szmielew. Podstawy geometrii. Państwowe Wydawnictwo Naukowe, Warszawa, 1955 (in Polish).Roland Coghetto. Homography in ℝℙ2. Formalized Mathematics, 24(4):239–251, 2016. doi:10.1515/forma-2016-0020.Roland Coghetto. Group of homography in real projective plane. Formalized Mathematics, 25(1):55–62, 2017. doi:10.1515/forma-2017-0005.Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21–32, 2018. doi:10.2478/forma-2018-0003.Roland Coghetto. Pascal’s theorem in real projective plane. Formalized Mathematics, 25 (2):107–119, 2017. doi:10.1515/forma-2017-0011.Adam Grabowski. Tarski’s geometry modelled in Mizar Computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11–14, 2016, pages 373–381, 2016. doi:10.15439/2016F290.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Kanchun, Hiroshi Yamazaki, and Yatsuka Nakamura. Cross products and tripple vector products in 3-dimensional Euclidean space. Formalized Mathematics, 11(4):381–383, 2003.Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master’s thesis.Yatsuka Nakamura. Graph theoretical properties of arcs in the plane and Fashoda Meet Theorem. Formalized Mathematics, 7(2):193–201, 1998.Karol Pąk and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143–150, 2007. doi:10.2478/v10037-007-0016-5.Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535–545, 1991.261334

  • Klein-Beltrami Model. Part I
    DeGruyter Open, 2018
    Co-Authors: Coghetto Roland
    Abstract:

    Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [3], [4], [14], [5]. With the Mizar system [2], [7] we use some ideas are taken from Tim Makarios’ MSc thesis [13] for the formalization of some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as further development of Tarski’s geometry in the formal setting [6]. Note that the model presented here, may also be called “Beltrami-Klein Model”, “Klein disk model”, and the “Cayley-Klein model” [1].Rue de la Brasserie 5, 7100 La Louvière, BelgiumNorbert A’Campo and Athanase Papadopoulos. On Klein’s so-called non-Euclidean geometry. arXiv preprint arXiv:1406.7309, 2014.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Eugenio Beltrami. Saggio di interpetrazione della geometria non-euclidea. Giornale di Matematiche, 6:284–322, 1868.Eugenio Beltrami. Essai d’interprétation de la géométrie non-euclidéenne. In Annales scientifiques de l’École Normale Supérieure. Trad. par J. Hoüel, volume 6, pages 251–288. Elsevier, 1869.Karol Borsuk and Wanda Szmielew. Podstawy geometrii. Państwowe Wydawnictwo Naukowe, Warszawa, 1955 (in Polish).Adam Grabowski. Tarski’s geometry modelled in Mizar Computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11–14, 2016, pages 373–381, 2016. doi:10.15439/2016F290.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Kanchun, Hiroshi Yamazaki, and Yatsuka Nakamura. Cross products and tripple vector products in 3-dimensional Euclidean space. Formalized Mathematics, 11(4):381–383, 2003.Artur Korniłowicz and Yasunari Shidama. Intersections of intervals and balls in Tn . Formalized Mathematics, 12(3):301–306, 2004.Artur Korniłowicz and Yasunari Shidama. Some properties of circles on the plane. Formalized Mathematics, 13(1):117–124, 2005.Akihiro Kubo. Lines in n -dimensional Euclidean spaces. Formalized Mathematics, 11(4): 371–376, 2003.Xiquan Liang, Piqing Zhao, and Ou Bai. Vector functions and their differentiation formulas in 3-dimensional Euclidean spaces. Formalized Mathematics, 18(1):1–10, 2010. doi:10.2478/v10037-010-0001-2.Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master’s thesis.Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535–545, 1991.Xiaopeng Yue, Xiquan Liang, and Zhongpin Sun. Some properties of some special matrices. Formalized Mathematics, 13(4):541–547, 2005.261213

  • Gauge Integral
    DeGruyter Open, 2017
    Co-Authors: Coghetto Roland
    Abstract:

    SummarySome authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [6]. The Lebesgue integral was formalized a little later [13] and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama [12].A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [10] and [4].Using the Mizar system [1], we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [a, b] (see [2], [3], [15], [14], [11]). In the next section we formalize that the Henstock-Kurzweil integral is linear.In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [6, 7, 8]) function over a interval a, b is Gauge integrable.Note that, in accordance with the possibilities of the MML [9], we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in [7] (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Robert G. Bartle. Return to the Riemann integral. American Mathematical Monthly, pages 625–632, 1996.Robert G. Bartle. A modern theory of integration, volume 32. American Mathematical Society Providence, 2001.Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 26(7):1196–1233, 2016.Roland Coghetto. Cousin’s lemma. Formalized Mathematics, 24(2):107–119, 2016. doi:10.1515/forma-2016-0009.Noboru Endou and Artur Korniłowicz. The definition of the Riemann definite integral and some related lemmas. Formalized Mathematics, 8(1):93–102, 1999.Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Darboux’s theorem. Formalized Mathematics, 9(1):197–200, 2001.Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Integrability of bounded total functions. Formalized Mathematics, 9(2):271–274, 2001.Adam Grabowski and Christoph Schwarzweller. Revisions as an essential tool to maintain mathematical repositories. In M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors, Towards Mechanized Mathematical Assistants. Lecture Notes in Computer Science, volume 4573, pages 235–249. Springer: Berlin, Heidelberg, 2007.John Harrison. Formalizing basic complex analysis. Studies in Logic, Grammar and Rhetoric, 23(10):151–165, 2007.Jean Mawhin. L’éternel retour des sommes de Riemann-Stieltjes dans l’évolution du calcul intégral. Bulletin de la Société Royale des Sciences de Liège, 70(4–6):345–364, 2001.Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. Riemann-Stieltjes integral. Formalized Mathematics, 24(3):199–204, 2016. doi:10.1515/forma-2016-0016.Yasunari Shidama, Noburu Endou, and Pauline N. Kawamoto. On the formalization of Lebesgue integrals. Studies in Logic, Grammar and Rhetoric, 10(23):167–177, 2007.Lee Peng Yee. The integral à la Henstock. Scientiae Mathematicae Japonicae, 67(1): 13–21, 2008.Lee Peng Yee and Rudolf Vyborny. Integral: an easy approach after Kurzweil and Henstock, volume 14. Cambridge University Press, 2000.25321722

Grabowski Adam - One of the best experts on this subject based on the ideXlab platform.

  • Tarski Geometry Axioms. Part IV – Right Angle
    DeGruyter Open, 2019
    Co-Authors: Coghetto Roland, Grabowski Adam
    Abstract:

    In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).Roland Coghetto - Rue de la Brasserie 5, 7100 La Louvi`ere, BelgiumAdam Grabowski - Institute of Informatics, University of Białystok, PolandGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.Michael Beeson and Larry Wos. OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning, volume 8562 of Lecture Notes in Computer Science, pages 495–510. Springer, 2014. doi:10.1007/978-3-319-08587-6 38.Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, Jan 2019. doi:10.1007/s10472-018-9606-x.Pierre Boutry, Gabriel Braun, and Julien Narboux. Formalization of the Arithmetization of Euclidean Plane Geometry and Applications. Journal of Symbolic Computation, 90: 149–168, 2019. doi:10.1016/j.jsc.2018.04.007.Pierre Boutry, Charly Gries, Julien Narboux, and Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, 62(1):1–68, 2019.Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289–313, 2017. doi:10.1515/forma-2017-0028.Sana Stojanovic Durdevic, Julien Narboux, and Predrag Janičić. Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249–269, 2015.Adam Grabowski. Tarski’s geometry modelled in Mizar Computerized proof assistant. In Maria Ganzha, Leszek Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of ACSIS – Annals of Computer Science and Information Systems, pages 373–381, 2016. doi:10.15439/2016F290.Adam Grabowski and Roland Coghetto. Tarski’s geometry and the Euclidean plane in Mizar. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Białystok, Poland, July 25–29, 2016, volume 1785 of CEUR-WS, pages 4–9, 2016.Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In Francisco Botana and Tomas Recio, editors, Automated Deduction in Geometry, pages 139–156, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. ISBN 978-3-540-77356-6.William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167–176, 2014. doi:10.2478/forma-2014-0017.Wolfram Schwabhcuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.271758

  • Formal Development of Rough Inclusion Functions
    DeGruyter Open, 2019
    Co-Authors: Grabowski Adam
    Abstract:

    Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article, continuing the formalization of rough sets [12], we give the formal characterization of three rough inclusion functions (RIFs). We start with the standard one, κ£, connected with Łukasiewicz [14], and extend this research for two additional RIFs: κ 1, and κ 2, following a paper by Gomolińska [4], [3]. We also define q-RIFs and weak q-RIFs [2]. The paper establishes a formal counterpart of [7] and makes a preliminary step towards rough mereology [16], [17] in Mizar [13].Institute of Informatics, University of Białystok, PolandAnna Gomolinska. A comparative study of some generalized rough approximations. Fundamenta Informaticae, 51:103–119, 2002.Anna Gomolinska. Rough approximation based on weak q-RIFs. In James F. Peters, Andrzej Skowron, Marcin Wolski, Mihir K. Chakraborty, and Wei-Zhi Wu, editors, Transactions on Rough Sets X, volume 5656 of Lecture Notes in Computer Science, pages 117–135, Berlin, Heidelberg, 2009. Springer. ISBN 978-3-642-03281-3. doi:10.1007/978-3-642-03281-3_4.Anna Gomolinska. On three closely related rough inclusion functions. In Marzena Kryszkiewicz, James F. Peters, Henryk Rybinski, and Andrzej Skowron, editors, Rough Sets and Intelligent Systems Paradigms, volume 4585 of Lecture Notes in Computer Science, pages 142–151, Berlin, Heidelberg, 2007. Springer. doi:10.1007/978-3-540-73451-2_16.Anna Gomolinska. On certain rough inclusion functions. In James F. Peters, Andrzej Skowron, and Henryk Rybinski, editors, Transactions on Rough Sets IX, volume 5390 of Lecture Notes in Computer Science, pages 35–55. Springer Berlin Heidelberg, 2008. doi:10.1007/978-3-540-89876-4_3.Adam Grabowski. On the Computer-assisted reasoning about rough sets. In B. Dunin-Kęplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi:10.1007/3-540-32370-8_15.Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129.Adam Grabowski. Building a framework of rough inclusion functions by means of Computerized proof assistant. In Tamás Mihálydeák, Fan Min, Guoyin Wang, Mohua Banerjee, Ivo Düntsch, Zbigniew Suraj, and Davide Ciucci, editors, Rough Sets, volume 11499 of Lecture Notes in Computer Science, pages 225–238, Cham, 2019. Springer International Publishing. ISBN 978-3-030-22815-6. doi:10.1007/978-3-030-22815-6_18.Adam Grabowski. Lattice theory for rough sets – a case study with Mizar. Fundamenta Informaticae, 147(2–3):223–240, 2016. doi:10.3233/FI-2016-1406.Adam Grabowski. Relational formal characterization of rough sets. Formalized Mathematics, 21(1):55–64, 2013. doi:10.2478/forma-2013-0006.Adam Grabowski. Binary relations-based rough sets – an automated approach. Formalized Mathematics, 24(2):143–155, 2016. doi:10.1515/forma-2016-0011.Adam Grabowski and Christoph Schwarzweller. On duplication in mathematical repositories. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, 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, volume 6167 of Lecture Notes in Computer Science, pages 300–314. Springer, 2010. doi:10.1007/978-3-642-14128-7_26.Adam Grabowski and Michał Sielwiesiuk. Formalizing two generalized approximation operators. Formalized Mathematics, 26(2):183–191, 2018. doi:10.2478/forma-2018-0016.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Jan Łukasiewicz. Die logischen Grundlagen der Wahrscheinlichkeitsrechnung. In L. Borkowski, editor, Jan Łukasiewicz – Selected Works, pages 16–63. North Holland, Polish Scientific Publ., Amsterdam London Warsaw, 1970. First published in Kraków, 1913.Zdzisław Pawlak. Rough sets. International Journal of Parallel Programming, 11:341–356, 1982. doi:10.1007/BF01001956.Lech Polkowski. Rough mereology. In Approximate Reasoning by Parts, volume 20 of Intelligent Systems Reference Library, pages 229–257, Berlin, Heidelberg, 2011. Springer. ISBN 978-3-642-22279-5. doi:10.1007/978-3-642-22279-5_6.Lech Polkowski and Andrzej Skowron. Rough mereology: A new paradigm for approximate reasoning. International Journal of Approximate Reasoning, 15(4):333–365, 1996. doi:10.1016/S0888-613X(96)00072-2.Andrzej Skowron and Jarosław Stepaniuk. Tolerance approximation spaces. Fundamenta Informaticae, 27(2/3):245–253, 1996. doi:10.3233/FI-1996-272311.William Zhu. Generalized rough sets based on relations. Information Sciences, 177: 4997–5011, 2007.27433734

  • Basic Formal Properties of Triangular Norms and Conorms
    DeGruyter Open, 2017
    Co-Authors: Grabowski Adam
    Abstract:

    SummaryIn the article we present in the Mizar system [1], [8] the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets [13]. The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality [2].After defining corresponding Mizar mode using four attributes, we introduced the following t-norms: minimum t-norm minnorm (Def. 6),product t-norm prodnorm (Def. 8),Łukasiewicz t-norm Lukasiewicz_norm (Def. 10),drastic t-norm drastic_norm (Def. 11),nilpotent minimum nilmin_norm (Def. 12),Hamacher product Hamacher_norm (Def. 13), and corresponding t-conorms: maximum t-conorm maxnorm (Def. 7),probabilistic sum probsum_conorm (Def. 9),bounded sum BoundedSum_conorm (Def. 19),drastic t-conorm drastic_conorm (Def. 14),nilpotent maximum nilmax_conorm (Def. 18),Hamacher t-conorm Hamacher_conorm (Def. 17). Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [10], [9]. It was proven formally that drastic-norm is the pointwise smallest t-norm and minnorm is the pointwise largest t-norm (maxnorm is the pointwise smallest t-conorm and drastic-conorm is the pointwise largest t-conorm). This work is a continuation of the development of fuzzy sets in Mizar [6] started in [11] and [3]; it could be used to give a variety of more general operations on fuzzy sets. Our formalization is much closer to the set theory used within the Mizar Mathematical Library than the development of rough sets [4], the approach which was chosen allows however for merging both theories [5], [7].Institute of Informatics, University of Białystok, PolandGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-817.Didier Dubois and Henri Prade. Fuzzy Sets and Systems: Theory and Applications. Academic Press, New York, 1980.Adam Grabowski. The formal construction of fuzzy numbers. Formalized Mathematics, 22(4):321–327, 2014. doi: 10.2478/forma-2014-0032.Adam Grabowski. On the Computer-assisted reasoning about rough sets. In B. Dunin-Kȩplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi: 10.1007/3-540-32370-815.Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi: 10.3233/FI-2014-1129.Adam Grabowski. On the Computer certification of fuzzy numbers. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, 2013 Federated Conference on Computer Science and Information Systems (FedCSIS), Federated Conference on Computer Science and Information Systems, pages 51–54, 2013.Adam Grabowski and Takashi Mitsuishi. Initial comparison of formal approaches to fuzzy and rough sets. In Leszek Rutkowski, Marcin Korytkowski, Rafal Scherer, Ryszard Tadeusiewicz, Lotfi A. Zadeh, and Jacek M. Zurada, editors, Artificial Intelligence and Soft Computing - 14th International Conference, ICAISC 2015, Zakopane, Poland, June 14-18, 2015, Proceedings, Part I, volume 9119 of Lecture Notes in Computer Science, pages 160–171. Springer, 2015. doi: 10.1007/978-3-319-19324-315.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi: 10.1007/s10817-015-9345-1.Petr Hájek. MetaMathematics of Fuzzy Logic. Dordrecht: Kluwer, 1998.Erich Peter Klement, Radko Mesiar, and Endre Pap. Triangular Norms. Dordrecht: Kluwer, 2000.Takashi Mitsuishi, Noboru Endou, and Yasunari Shidama. The concept of fuzzy set and membership function and basic properties of fuzzy set operation. Formalized Mathematics, 9(2):351–356, 2001.Takashi Mitsuishi, Katsumi Wasaki, and Yasunari Shidama. Basic properties of fuzzy set operation and membership function. Formalized Mathematics, 9(2):357–362, 2001.Lotfi Zadeh. Fuzzy sets. Information and Control, 8(3):338–353, 1965.2529310

  • Tarski Geometry Axioms – Part II
    De Gruyter Open, 2016
    Co-Authors: Coghetto Roland, Grabowski Adam
    Abstract:

    In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation),of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1),congruence equivalence relation (A2),congruence identity (A3),segment construction (A4),SAS (A5),betweenness identity (A6),Pasch (A7). Also a simple model, which satisfies these axioms, was previously constructed, and described in [6]. In this paper, we deal with four remaining axioms, namely: the lower dimension axiom (A8),the upper dimension axiom (A9),the Euclid axiom (A10),the continuity axiom (A11). They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles cong is introduced via congruence of sides (SSS).In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure Euclid 2 satisfies all these attributes.Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].Coghetto Roland - Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrabowski Adam - Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, PolandCzesław Byliński. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99–107, 2005.Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.Roland Coghetto. Circumcenter, circumcircle and centroid of a triangle. Formalized Mathematics, 24(1):17–26, 2016. doi:10.1515/forma-2016-0002.Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129.Adam Grabowski. Tarski’s geometry modelled in Mizar Computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11–14, 2016, pages 373–381, 2016. doi:10.15439/2016F290.Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5.Adam Grabowski and Christoph Schwarzweller. On duplication in mathematical repositories. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, 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, volume 6167 of Lecture Notes in Computer Science, pages 300–314. Springer, 2010. doi:10.1007/978-3-642-14128-7_26.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. 2012. Master’s thesis.Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In F. Botana and T. Recio, editors, Automated Deduction in Geometry, volume 4869 of Lecture Notes in Computer Science, pages 139–156. Springer, 2007.William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167–176, 2014. doi:10.2478/forma-2014-0017.Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.Alfred Tarski and Steven Givant. Tarski’s system of geometry. Bulletin of Symbolic Logic, 5(2):175–214, 1999.Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.Wojciech A. Trybulec. Axioms of incidence. Formalized Mathematics, 1(1):205–213, 1990.Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990

Shidama Yasunari - One of the best experts on this subject based on the ideXlab platform.

  • Continuity of Multilinear Operator on Normed Linear Spaces
    DeGruyter Open, 2019
    Co-Authors: Nakasho Kazuhisa, Shidama Yasunari
    Abstract:

    In this article, various definitions of contuity of multilinear operators on normed linear spaces are discussed in the Mizar formalism [4], [1] and [2]. In the first chapter, several basic theorems are prepared to handle the norm of the multilinear operator, and then it is formalized that the linear space of bounded multilinear operators is a complete Banach space.In the last chapter, the continuity of the multilinear operator on finite normed spaces is addressed. Especially, it is formalized that the continuity at the origin can be extended to the continuity at every point in its whole domain. We referred to [5], [11], [8], [9] in this formalization.Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, JapanYasunari Shidama - Shinshu University, Nagano, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.Noboru Endou, Yasunari Shidama, and Keiichi Miyajima. The product space of real normed spaces and its properties. Formalized Mathematics, 15(3):81–85, 2007. doi:10.2478/v10037-007-0010-y.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39–48, 2004.Kosaku Yoshida. Functional Analysis. Springer, 1980.271616

  • Continuity of Bounded Linear Operators on Normed Linear Spaces
    DeGruyter Open, 2018
    Co-Authors: Nakasho Kazuhisa, Futa Yuichi, Shidama Yasunari
    Abstract:

    In this article, using the Mizar system [1], [2], we discuss the continuity of bounded linear operators on normed linear spaces. In the first section, it is discussed that bounded linear operators on normed linear spaces are uniformly continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.This study was supported in part by JSPS KAKENHI Grant Number JP17K00182.Kazuhisa Nakasho - Yamaguchi University, Yamaguchi, JapanYuichi Futa - Tokyo University of Technology, Tokyo, JapanYasunari Shidama - Shinshu University, Nagano, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.N. J. Dunford and T. Schwartz. Linear operators I. Interscience Publ., 1958.Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Topological properties of real normed space. Formalized Mathematics, 22(3):209–223, 2014. doi:10.2478/forma-2014-0024.Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.Keiko Narita, Noboru Endou, and Yasunari Shidama. Riemann integral of functions from ℝ into real Banach space. Formalized Mathematics, 21(2):145–152, 2013. doi:10.2478/forma-2013-0016.Takaya Nishiyama, Artur Korniłowicz, and Yasunari Shidama. The uniform continuity of functions on normed linear spaces. Formalized Mathematics, 12(3):277–279, 2004.Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269–275, 2004.Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51–59, 2011. doi:10.2478/v10037-011-0009-2.Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39–48, 2004.Yasunari Shidama. The series on Banach algebra. Formalized Mathematics, 12(2):131–138, 2004.Kosaku Yoshida. Functional Analysis. Springer, 1980.26323123

  • Dual Lattice of ℤ-module Lattice
    DeGruyter Open, 2017
    Co-Authors: Futa Yuichi, Shidama Yasunari
    Abstract:

    SummaryIn this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].Futa Yuichi - Tokyo University of Technology, Tokyo, JapanShidama Yasunari - Shinshu University, Nagano, JapanGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007/978-3-319-20615-817.Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.Yuichi Futa and Yasunari Shidama. Lattice of ℤ-module. Formalized Mathematics, 24 (1):49–68, 2016. doi: 10.1515/forma-2016-0005.Yuichi Futa and Yasunari Shidama. Embedded lattice and properties of Gram matrix. Formalized Mathematics, 25(1):73–86, 2017. doi: 10.1515/forma-2017-0007.Yuichi Futa and Yasunari Shidama. Divisible ℤ-modules. Formalized Mathematics, 24 (1):37–47, 2016. doi: 10.1515/forma-2016-0004.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47–59, 2012. doi: 10.2478/v10037-012-0007-z.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of ℤ-module. Formalized Mathematics, 20(3):205–214, 2012. doi: 10.2478/v10037-012-0024-y.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of ℤ-module. Formalized Mathematics, 23(1):29–49, 2015. doi: 10.2478/forma-2015-0003.Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841–845, 1990.Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515–534, 1982. doi: 10.1007/BF01457454.Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1 (3):495–500, 1990.Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877–882, 1990.Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883–885, 1990.Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990.25215716

  • F. Riesz Theorem
    DeGruyter Open, 2017
    Co-Authors: Narita Keiko, Nakasho Kazuhisa, Shidama Yasunari
    Abstract:

    SummaryIn this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].Narita Keiko - Hirosaki-city, Aomori, JapanNakasho Kazuhisa - Akita Prefectural University, Akita, JapanShidama Yasunari - Shinshu University, Nagano, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011.Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.Katuhiko Kanazashi, Noboru Endou, and Yasunari Shidama. Banach algebra of continuous functionals and the space of real-valued continuous functionals with bounded support. Formalized Mathematics, 18(1):11–16, 2010. doi:10.2478/v10037-010-0002-1.Kazuhisa Nakasho, Keiko Narita, and Yasunari Shidama. The basic existence theorem of Riemann-Stieltjes integral. Formalized Mathematics, 24(4):253–259, 2016. doi:10.1515/forma-2016-0021.Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69–77, 2014. doi:10.2478/forma-2014-0007.Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. Riemann-Stieltjes integral. Formalized Mathematics, 24(3):199–204, 2016. doi:10.1515/forma-2016-0016.Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.Yasunari Shidama, Hikofumi Suzuki, and Noboru Endou. Banach algebra of bounded functionals. Formalized Mathematics, 16(2):115–122, 2008. doi:10.2478/v10037-008-0017-z.Kosaku Yoshida. Functional Analysis. Springer, 1980.25317918

  • Isomorphism Theorem on Vector Spaces over a Ring
    DeGruyter Open, 2017
    Co-Authors: Futa Yuichi, Shidama Yasunari
    Abstract:

    SummaryIn this article, we formalize in the Mizar system [1, 4] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [5] base reduction algorithm and cryptographic systems [6, 2].Futa Yuichi - Tokyo University of Technology, Tokyo, JapanShidama Yasunari - Shinshu University, Nagano, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Submodule of free ℤ-module. Formalized Mathematics, 21(4):273–282, 2013. doi:10.2478/forma-2013-0029.Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515–534, 1982. doi:10.1007/BF01457454.Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.Yasunari Shidama. Differentiable functions on normed linear spaces. Formalized Mathematics, 20(1):31–40, 2012. doi:10.2478/v10037-012-0005-1.25317117

Ягуп, Екатерина Валериевна - One of the best experts on this subject based on the ideXlab platform.

  • Research of the modes of full compensation of reactive power in a three-phase power supply system
    Национальный технический университет "Харьковский политехнический институт", 2019
    Co-Authors: Ягуп, Валерий Григорьевич, Ягуп, Екатерина Валериевна
    Abstract:

    Рассматривается решение задачи определения параметров режимов полной компенсации реактивной мощности для трехфазной системы с линейной несимметричной нагрузкой. Исследования, проведенные с помощью SimPowerSystems-модели и метода деформируемого многогранника, показали, что в зависимости от начальных условий для переменных оптимизации, процесс оптимизации может приводить к двум различным решениям. Основной режим полной компенсации характеризуется существенным уменьшением потерь в системе. Второй же, дополнительный режим полной компенсации может характеризоваться неприемлемыми на практике возрастаниями токов и напряжений в системе электроснабжения.The article is devoted to the issues of current balancing and reactive power compensation in a three-phase power supply system. Optimal in all these respects is the mode of full compensation of reactive power, by which we mean such a symmetrical mode, in which only active power is consumed from the source. The task of calculating the mode of full reactive power compensation is non-linear and can be solved using non-linear optimization methods based on the adopted parameters and optimization criteria. The objective of the article is to develop a visual model of the power supply system with an unbalanced load, in which current balancing and reactive power compensation is performed using a symmetrical-compensating device, which parameters are determined using search non-linear optimization tools and modern Computer Mathematics software packages. The purpose of the article is to research the modes of full compensation of reactive power in a three-phase power supply system with a linear asymmetric load in order to identify the ambiguity of solving the problem of synthesizing parameters of a reactive power compensator. Methodology of research consists in the development of a visual model of a power supply system that feeds unbalanced load. As a symmetrical compensating device, capacitors connected between the phases of the transmission line are used. The model is controlled by a program that launches the model and performs optimization and selection of optimization variable values. The optimization values are the capacitors of the symmetry-compensating device. The optimization criterion is a spherical metric consisting of the reactive powers of each source of electricity. Results lead depending on the choice of the initial values of the optimization variables, the optimization process enters two modes of full compensation of reactive power – main and additional. The main mode is characterized by small values of capacitors and small values of currents, and in the additional mode, these values of the system and operational parameters reach extremely large values that are unacceptable for practical use. Originality liesin the fact that in terms of optimization theory this means that there is no global optimum in the solution of the problem of full compensation, however, there are two local optimums. Both modes are stable, as evidenced by modeling on the SPS-model of the system in the time domain in the space of state variables. Practical significance of the work lies in the fact that when designing a microprocessor system that optimizes the operating mode of the power supply system, it is necessary to envisage the situation of additional mode

E. V. Yagup - One of the best experts on this subject based on the ideXlab platform.

  • RESEARCH OF THE MODES OF FULL COMPENSATION OF REACTIVE POWER IN A THREE-PHASE POWER SUPPLY SYSTEM
    Kharkiv Polytechnic Institute, 2019
    Co-Authors: V. G. Yagup, E. V. Yagup
    Abstract:

    Introduction The article is devoted to the issues of current balancing and reactive power compensation in a three-phase power supply system. Optimal in all these respects is the mode of full compensation of reactive power, by which we mean such a symmetrical mode, in which only active power is consumed from the source. The task of calculating the mode of full reactive power compensation is non-linear and can be solved using non-linear optimization methods based on the adopted parameters and optimization criteria. The objective of the article is to develop a visual model of the power supply system with an unbalanced load, in which current balancing and reactive power compensation is performed using a symmetrical-compensating device, which parameters are determined using search non-linear optimization tools and modern Computer Mathematics software packages. The purpose of the article is to research the modes of full compensation of reactive power in a three-phase power supply system with a linear asymmetric load in order to identify the ambiguity of solving the problem of synthesizing parameters of a reactive power compensator. Methodology of research consists in the development of a visual model of a power supply system that feeds unbalanced load. As a symmetrical compensating device, capacitors connected between the phases of the transmission line are used. The model is controlled by a program that launches the model and performs optimization and selection of optimization variable values. The optimization values are the capacitors of the symmetry-compensating device. The optimization criterion is a spherical metric consisting of the reactive powers of each source of electricity. Results lead depending on the choice of the initial values of the optimization variables, the optimization process enters two modes of full compensation of reactive power – main and additional. The main mode is characterized by small values of capacitors and small values of currents, and in the additional mode, these values of the system and operational parameters reach extremely large values that are unacceptable for practical use. Originality lies in the fact that in terms of optimization theory this means that there is no global optimum in the solution of the problem of full compensation, however, there are two local optimums. Both modes are stable, as evidenced by modeling on the SPS-model of the system in the time domain in the space of state variables. Practical significance of the work lies in the fact that when designing a microprocessor system that optimizes the operating mode of the power supply system, it is necessary to envisage the situation of additional mode