Zobrazeno 1 - 10
of 29
pro vyhledávání: '"Grzegorz Bancerek"'
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
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 24, Iss 2, Pp 95-106 (2016)
Summary Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M 1 such that M 1(x) > N 1(x) and (∀y ∈ N 1)x ⊀ y.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7235236b92219486affc8b9fbea98911
https://doi.org/10.1515/forma-2016-0008
https://doi.org/10.1515/forma-2016-0008
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
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 22, Iss 3, Pp 225-255 (2014)
Summary We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b30341fc5285741a1a954f9a7358fc5f
https://doaj.org/article/c18f9191bf90418fabdcf079f7d71a64
https://doaj.org/article/c18f9191bf90418fabdcf079f7d71a64
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 22, Iss 2, Pp 125-155 (2014)
Summary Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be3cfe12d150a9ec6fef95ac52d56d9c
https://doaj.org/article/8af1807ebdc54d2b8fdb4cfd360f182e
https://doaj.org/article/8af1807ebdc54d2b8fdb4cfd360f182e
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 22, Iss 1, Pp 37-56 (2014)
Reduction Systems and Idea of Knuth-Bendix Completion Algorithm Grzegorz Bancerek Association of Mizar Users Bialystok, Poland Summary. Educational content for abstract reduction systems concerning reduction, convertibility, normal forms, divergence
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::56c68c724dd5d898512585b76a7b4ac0
https://doaj.org/article/eb93587eefb04e01af3ac16bade92b3e
https://doaj.org/article/eb93587eefb04e01af3ac16bade92b3e
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 21, Iss 1, Pp 41-46 (2013)
In this paper X denotes a set, R, R1, R2 denote binary relations, x, y, z denote sets, and n, m, k denote natural numbers. Let us consider a binary relation R on X. Now we state the propositions: (1) fieldR ⊆ X. (2) If x, y ∈ R, then x, y ∈ X.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::763e2a610200c68f56130972feac6f08
https://doi.org/10.2478/forma-2013-0004
https://doi.org/10.2478/forma-2013-0004
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 21, Iss 1, Pp 1-23 (2013)
Now we state the propositions: (1) (i) 1 mod 2 = 1, and (ii) 2 mod 2 = 0. (2) Let us consider a non empty non void many sorted signature Σ, an algebra A over Σ, a subalgebra B of A, a sort symbol s of Σ, and a set a. Suppose a ∈ (the sorts of B)
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::af456217da060201af7b9574c7eff17d
https://doaj.org/article/5b8f2e228c4842118b80826db948a4be
https://doaj.org/article/5b8f2e228c4842118b80826db948a4be
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 20, Iss 3, Pp 239-256 (2012)
Summary We interoduce a new characterization of algebras of normal forms of term rewriting systems [35] as algerbras of term free in itself (any function from free generators into the algebra generates endomorphism of the algebra). Introduced algebra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8d1831f7ecf94ca84865b628f4783b61
https://doaj.org/article/2b64bc4a66004b518e4b3ed20ecd153c
https://doaj.org/article/2b64bc4a66004b518e4b3ed20ecd153c
Autor:
Grzegorz Bancerek
Publikováno v:
Formalized Mathematics, Vol 20, Iss 4, Pp 309-341 (2012)
Summary We introduce an algebra with free variables, an algebra with undefined values, a program algebra over a term algebra, an algebra with integers, and an algebra with arrays. Program algebra is defined as universal algebra with assignments. Prog
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::778539b5eca37c43a978fc853d9a55d2
https://doaj.org/article/e7c7d6c5ec4f4b25aa2851486dca7475
https://doaj.org/article/e7c7d6c5ec4f4b25aa2851486dca7475