16 research outputs found
Basic first-order model theory in Mizar
No full textThe author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.
In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.
This is an overview and commentary on some key aspects of this setup.
It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done
Pencegahan Paham Radikalisme Lewat Penguatan Moderasi Beragama Melalui Ekstrakurikuler Rohani Islam
No full textPenguatan moderasi beragama dinilai penting untuk dibangun dalam mewujudkan sikap beragama yang damai dan penuh toleransi. Upaya penguatan moderasi beragama tentu diperlukan kepada generasi muda khususnya siswa sekolah dengan memanfaatkan organisasi kesiswaan seperti Rohani Islam. Tujuan penelitian ini adalah untuk menguraikan fungsi Rohani Islam dalam penguatan moderasi beragama, menguraikan implementasi penguatan moderasi beragama melalui Rohani Islam dan mendeskripsikan implikasi dari penguatan moderasi beragama melalui rohani Islam di SMA Negeri 1 Binjai. Metode penelitian yang digunakan adalah kualitatif deskriptif, proses pengumpulan data dilakukan melalui observasi secara langsung, wawancara dan studi dokumentasi. Hasil penelitian menemukan bahwa Rohani Islam berfungsi strategis dalam penguatan moderasi beragama di SMA Negeri 1 Binjai. Implementasi penguatan moderasi beragama dilakukan melalui sebuah kegiatan kelompok bersama yang mencakup seluruh siswa dengan agama berbeda dan melalui kampanye moderasi beragama lewat youtube dan media sosial. Implikasi penguatan moderasi beragama terlihat pada peningkatan sikap moderasi beragama siswa di lingkungan sekolah yang tercermin dalam sikap berteman siswa yang tidak membeda-bedakan ras, suku, budaya dan agama. Dengan demikian, melalui penelitian ini dapat disimpulkan bahwa penguatan moderasi beragama melalui Rohani Islam dapat meningkatkan sikap moderasi beragama siswa di SMA Negeri 1 Binjai
Systémy pro formální matematiku
No full textTitle: Systems for formal mathematics Author: Ondrěj Kuncˇar Department: Dep. of Theoretical Computer Science and Mathematical Logic Supervisor: Mgr. Josef Urban, Ph.D. Supervisor's e-mail address: [email protected] Abstract: The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subty- ping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at recon- struction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mi- zar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction. Keywords: type system, Mizar, HOL Light
Islamisasi sains: Sebuah Kajian Analisis Paradigma Transdisipliner di Prodi Magister PAI UIN Sumatera Utara
Get PDFTransdisipliner merupakan sebuah pendekatan dalam pemecahan sebuah masalah dengan melakukan peninjauan ilmu yang relatif dikuasai dan relevan dengan permasalahan yang akan dipecahkan meskipun berada di luar kemampuan dan keahlian sebagai hasil pendidikan formal lewat orang yang memecah masalah tersebut. Tujuan penelitian ini adalah Untuk memahami Islamisasi Sains Berbasis Transdisipliner dalam sudut pandang keilmuan di Prodi Magister PAI UIN Sumatera Utara. kemudian Strategi pengembangan paradigma keilmuan berbasis transdisipliner di Prodi Magister PAI UIN Sumatera Utara. selanjutnya hambatan dalam pengambangan paradigma keilmuan berbasis transdisipliner di Prodi Magister PAI UIN Sumatera Utara. Metode penelitian ini ialah penelitian Kualitatif dimana menjelaskan secara jelas terkait hal-hal yang terjadi di lapangan. Hasil dari penelitian ini adalah Hasil dari penelitian ini adalah bahwa islamisasi sains adalah sebuah hal yang di jadikan sebagai paradigma baru Pendidikan islam. Perwujudan itu dituangkan di UIN Sumatera Utara dengan paradigma integrasi ilmu wahdatul ulum dengan pendekatan transdisipliner. Dalam proses pembelajaran di Prodi Magister PAI UIN Sumatera Utara dilakukan dengan mengedepankan pembelajaran berbasis pendekatan Transdisipliner. Strategi yang dikembangkan adalah dengan pengambangan kelembagaan, kurikulum dan peningkatan kompetensi guru. Hambatannya ialah terkait sosialisasi, pandangan paradigma dosen dan optimalisasi implementas
Fubini’s Theorem
Get PDFFubini theorem is an essential tool for the analysis of high-dimensional space [8], [2], [3], a theorem about the multiple integral and iterated integral. The author has been working on formalizing Fubini’s theorem over the past few years [4], [6] in the Mizar system [7], [1]. As a result, Fubini’s theorem (30) was proved in complete form by this article.National Institute of Technology, Gifu College, 2236-2 Kamimakuwa, Motosu, Gifu, JapanGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 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.Heinz Bauer. Measure and Integration Theory. Walter de Gruyter Inc., 2002.Vladimir Igorevich Bogachev and Maria Aparecida Soares Ruas. Measure theory, volume 1. Springer, 2007.Noboru Endou. Fubini’s theorem on measure. Formalized Mathematics, 25(1):1–29, 2017. doi:10.1515/forma-2017-0001.Noboru Endou. Integral of non positive functions. Formalized Mathematics, 25(3):227–240, 2017. doi:10.1515/forma-2017-0022.Noboru Endou. Fubini’s theorem for non-negative or non-positive functions. Formalized Mathematics, 26(1):49–67, 2018. doi:10.2478/forma-2018-0005.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.P. R. Halmos. Measure Theory. Springer-Verlag, 1974.271677
Binary Representation of Natural Numbers
Get PDFThis study was supported in part by JSPS KAKENHI Grant Numbers JP17K00182. The author would also like to express gratitude to Prof. Yasunari Shidama for his support and encouragement.Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.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.Donald E. Knuth. The Art of Computer Programming, Volume 1: Fundamental Algorithms, Third Edition. Addison-Wesley, 1997.Hisayoshi Kunimune and Yatsuka Nakamura. A representation of integers by binary arithmetics and addition of integers. Formalized Mathematics, 11(2):175–178, 2003.Gottfried Wilhelm Leibniz. Explication de l’Arithmétique Binaire, volume 7. C. Gerhardt, Die Mathematische Schriften edition, 223 pages, 1879.Robert Milewski. Binary arithmetics. Binary sequences. Formalized Mathematics, 7(1): 23–26, 1998.Yasuho Mizuhara and Takaya Nishiyama. Binary arithmetics, addition and subtraction of integers. Formalized Mathematics, 5(1):27–29, 1996.Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4 (1):83–86, 1993.26322322
and Bi-Modules over a Ring
No full textWe offer to our Readers Volume 2 of mathematical papers which are abstracts of Mizar articles to be found in the Main Mizar Library (MML). They are usually published in the order in which they have been approved for MML. A careful Reader may note that our publication has several peculiarities due to two facts. First, it is an endeavour to make a machine translation into English. Secondly, changes in the PC Mizar system and continually updated MML influence the quality of the texts published and the topical value of the papers. Hence, first, the standard of English is not always satisfactory. Secondly, the quality of the papers is very closely related to what is actually taking place in MML. Originally, obvious theorems (relative to the power of Checker) were not identified. As the system PC Mizar was developing, some theorems became obvious. It is likewise with repeated theorems (which accounts for the footnotes in the text of the type ”The proposition (k) was either repeated or obvious”). Those theorems can be classed in two groups. The first includes accidental repetitions: the author did not know that such a theorem was already included in MML and proved it again. There were few such cases. The other includes some 500 eliminated theorems because they were so-called definitional theorems. The authors wrote those theorems because previously it had not been possible directly to refer to definitions. The Readers are also requested to note that in the present issue we have changed the formats of certain operations. The operation symbol of the removal of n initial terms from a sequence has been changed from into ↑ (see [2] and [1]). Likewise, the operation symbol of the multiplication of real functions ⋄ has been removed (see [1])
Strengthening Religious Moderation through Islamic Spirituality at State Senior High School 1 Binjai
Get PDFStrengthening religious moderation It is important to instill religious moderation in the younger generation such as school students. Because in fact, there are many cases where students have a radical understanding of religion. in religion, this happens due to the indoctrination of radical ideas to students through da'wah institutions at school. Therefore, researchers formulated this research with the title "Strengthening Religious Moderation through Islamic Spirituality at SMA Negeri 1 Binjang Through Islamic Spirituality at SMA Negeri 1 Binjai". The purpose of the research is to outline the function of Islamic Spirituality in strengthening religious moderation, know the form of implementation of strengthening religious moderation through Islamic Spirituality and describe the implications of strengthening religious moderation through the Islamic Spirituality at SMA Negeri 1 Binjai. The method used in the research is descriptive qualitative research is a method used to research the conditions of objects that occur naturally and at the same time the researcher becomes the key instrument. becomes the key instrument. Data collection techniques are done through observation, interviews and documentation studies. Data analysis is done with interactive analysis techniques. interactive analysis techniques. The results showed that Islamic Spirituality functions strategically in strengthening religious moderation at SMA Negeri 1 Binjai, the implementation of strengthening religious moderation is carried out with the activities of Romansa Greeting and proselytizing campaigns via YouTube and social media, the implications can be seen by the increase in students' religious moderation in the environment. can be seen by the increase in students' religious moderation attitudes in the school environment
Tarski Geometry Axioms
No full textThis is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work.
The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms.
This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line.
The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.Richter William - Departament of Mathematics Nortwestern University Evanston, USAGrabowski Adam - Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok PolandAlama Jesse - Technical University of Vienna AustriaGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 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.Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In F. Botana and T. Recio, editors, Automated Deduction in Geometry, volume 4869, pages 139–156, 2007.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.Wojciech A. Trybulec. Axioms of incidence. Formalized Mathematics, 1(1):205–213, 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. Received June 16, 201
Lim-inf convergence and its compactness
No full textAbstract- We describe the Mizar formalization of the proof of compactness of lim-inf convergence given in [W33] according to [CCL]. Lim-inf convergence formalized in [W28] is a Moore-Smith convergence investigated in [Y6] and involves the concept of nets. The proof is based on the equivalence of two approaches to convergence in topological spaces: filter convergence and Moore-Smith (net) convergence. The equivalence is worked out in [Y19] and different characterizations of compactness are also given there. These efforts are a continuation of the international project of formalizing the theory of continuous lattices headed by the first author
