http://hdl.handle.net/11320/3660 2026-06-01T19:15:57Z 2026-06-01T19:15:57Z Grabowski, Adam http://hdl.handle.net/11320/3673 2017-10-05T22:56:42Z 2013-01-01T00:00:00Z

Tytuł: Relational Formal Characterization of Rough Sets Autorzy: Grabowski, Adam Abstrakt: The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based models of rough sets [12] trying to formalize some parts of [19] following also [18] in some sense (Propositions 1-8, Corr. 1 and 2; the complete description is available in the Mizar script). Our main problem was that informally, there is a direct correspondence between relations and underlying properties, in our approach however [7], which uses relational structures rather than relations, we had to switch between classical (based on pure set theory) and abstract (using the notion of a structure) parts of the Mizar Mathematical Library. Our next step will be translation of these properties into the pure language of Mizar attributes.

2013-01-01T00:00:00Z Rowinska-Schwarzweller, Agnieszka Schwarzweller, Christoph http://hdl.handle.net/11320/3672 2017-10-05T22:56:41Z 2013-01-01T00:00:00Z

Tytuł: A Test for the Stability of Networks Autorzy: Rowinska-Schwarzweller, Agnieszka; Schwarzweller, Christoph Abstrakt: A complex polynomial is called a Hurwitz polynomial, if all its roots have a real part smaller than zero. This kind of polynomial plays an all-dominant role in stability checks of electrical (analog or digital) networks. In this article we prove that a polynomial p can be shown to be Hurwitz by checking whether the rational function e(p)/o(p) can be realized as a reactance of one port, that is as an electrical impedance or admittance consisting of inductors and capacitors. Here e(p) and o(p) denote the even and the odd part of p [25].

2013-01-01T00:00:00Z Bancerek, Grzegorz http://hdl.handle.net/11320/3671 2017-10-05T22:56:41Z 2013-01-01T00:00:00Z

Tytuł: Semantics of MML Query - Ordering Autorzy: Bancerek, Grzegorz Abstrakt: Semantics of order directives of MML Query is presented. The formalization is done according to [1]

2013-01-01T00:00:00Z Okazaki, Hiroyuki Yamazaki, Hiroshi Shidama, Yasunari http://hdl.handle.net/11320/3674 2017-10-05T22:57:28Z 2013-01-01T00:00:00Z

Tytuł: Isomorphisms of Direct Products of Finite Commutative Groups Autorzy: Okazaki, Hiroyuki; Yamazaki, Hiroshi; Shidama, Yasunari Abstrakt: We have been working on the formalization of groups. In [1], we encoded some theorems concerning the product of cyclic groups. In this article, we present the generalized formalization of [1]. First, we show that every finite commutative group which order is composite number is isomorphic to a direct product of finite commutative groups which orders are relatively prime. Next, we describe finite direct products of finite commutative groups.

2013-01-01T00:00:00Z