Zobrazeno 1 - 10
of 32
pro vyhledávání: '"Adam Naumowicz"'
Publikováno v:
Journal of Formalized Reasoning, Vol 3, Iss 2, Pp 153-245 (2010)
This paper is intended to be a practical reference manual for basic Mizar terminology which may be helpful to get started using the system. The paper describes most important aspects of the Mizar language as well as some features of the verification
Externí odkaz:
https://doaj.org/article/b94db71521544edb9e5060f349e1cba9
Autor:
Artur Kornilowicz, Adam Naumowicz
Publikováno v:
Formalized Mathematics. 30:229-234
Summary This paper reports on the formalization of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [5] using the Mizar system [4], [1], [2]. Problems 12, 13, 31, 32, 33, 35 and 40 belong to the chapter
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::98588c77c3879679de544e7e76fbbe96
https://doi.org/10.2478/forma-2022-0018
https://doi.org/10.2478/forma-2022-0018
Autor:
Adam Naumowicz
Publikováno v:
Formalized Mathematics, Vol 28, Iss 1, Pp 115-120 (2020)
Summary In this paper we demonstrate the feasibility of formalizing recreational mathematics in Mizar ([1], [2]) drawing examples from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [4]. The current work contains proofs of init
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::57c723d03df97baebbfd6b3f6b22136a
https://doaj.org/article/cdf98613e70c4554a56be885aac8db97
https://doaj.org/article/cdf98613e70c4554a56be885aac8db97
Autor:
Adam Naumowicz
Publikováno v:
SYNASC
This paper presents the extended processing of adjectives with visible arguments in the Mizar system. The proposed enhancement is compared with the current implementation by presenting the results of a case study based on refactoring selected Mizar M
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::da4bd8032a5f3861e7da10fa0d2467a1
https://doi.org/10.1109/synasc51798.2020.00026
https://doi.org/10.1109/synasc51798.2020.00026
Autor:
Adam Naumowicz
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030535179
CICM
CICM
In this paper we present a dataset based on the Mizar formalization of selected problems related to elementary number theory. The dataset comprises proofs of problems on several levels of difficulty. They are available in the form of full proofs, pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::841b6118f2375f39cf687fd415f17efd
https://doi.org/10.1007/978-3-030-53518-6_22
https://doi.org/10.1007/978-3-030-53518-6_22
Autor:
Grzegorz Bancerek, Czesław Byliński, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Adam Grabowski, Karol Pąk
Publikováno v:
Journal of Automated Reasoning
The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an important mile
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::966fc698f4f694d59c6a26ccc377834a
http://europepmc.org/articles/PMC6044251
http://europepmc.org/articles/PMC6044251
Publikováno v:
Formalized Mathematics, Vol 25, Iss 1, Pp 49-54 (2017)
Summary In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e4c3ae8b03db78f866e6b09b02472a83
https://doi.org/10.1515/forma-2017-0004
https://doi.org/10.1515/forma-2017-0004
Autor:
Adam Naumowicz, Artur Korniłowicz
Publikováno v:
Formalized Mathematics, Vol 24, Iss 4, Pp 301-308 (2016)
Summary This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::447b4b10bbf6f61d33e9372d172ea98a
https://doaj.org/article/b6343f726d65400ca69dec2d4d4f12a0
https://doaj.org/article/b6343f726d65400ca69dec2d4d4f12a0
Publikováno v:
Intelligent Computer Mathematics-11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings
Lecture Notes in Computer Science ISBN: 9783319968117
CICM
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Intelligent Computer Mathematics
Lecture Notes in Computer Science ISBN: 9783319968117
CICM
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Intelligent Computer Mathematics
We describe a new version of the Mizar-to- Open image in new window translator. The system has been re-implemented as XSL stylesheets instead of as Pascal programs, allowing greater flexibility. It can now be used to generate both Open image in new w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0e1cf75710445a771ddcb585f1ccd043
Publikováno v:
Journal of Automated Reasoning. 55:191-198
This special issue is dedicated to works related to Mizar, the theorem proving project started by Andrzej Trybulec in the 1970s, and other automated proof checking systems used for formalizing mathematics.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9c01d351c084ccb0a990579d7cfef0e6
https://doi.org/10.1007/s10817-015-9345-1
https://doi.org/10.1007/s10817-015-9345-1