<abstract xmlns="http://www.w3.org/1999/xhtml">Rough sets, developed by Zdzisław Pawlak <xref ref-type="bibr" rid="j_forma-2016-0011_ref_012_w2aab2b8b3b1b7b1ab1ac12Aa">[12]</xref>, are an important tool to describe the state of incomplete or partially unknown information. In this article, which is essentially the continuation of <xref ref-type="bibr" rid="j_forma-2016-0011_ref_008_w2aab2b8b3b1b7b1ab1ab8Aa">[8]</xref>, 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 <xref ref-type="bibr" rid="j_forma-2016-0011_ref_011_w2aab2b8b3b1b7b1ab1ac11Aa">[11]</xref>). Here we drop the classical equivalence- and tolerance-based models of rough sets trying to formalize some parts of <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>.The main aim of this Mizar article is to provide a formal counterpart for the rest of the paper of William Zhu <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>. In order to do this, we recall also Theorem 3 from Y.Y. Yao’s paper <xref ref-type="bibr" rid="j_forma-2016-0011_ref_017_w2aab2b8b3b1b7b1ab1ac17Aa">[17]</xref>. The first part of our formalization (covering first seven pages) is contained in <xref ref-type="bibr" rid="j_forma-2016-0011_ref_008_w2aab2b8b3b1b7b1ab1ab8Aa">[8]</xref>. Now we start from page 5003, sec. 3.4. <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>. We formalized almost all numbered items (definitions, propositions, theorems, and corollaries), with the exception of Proposition 7, where we stated our theorem only in terms of singletons. We provided more thorough discussion of the property <italic>positive alliance</italic> and its connection with seriality and reflexivity (and also transitivity). Examples were not covered as a rule as we tried to construct a more general mechanism of finding appropriate models for approximation spaces in Mizar providing more automatization than it is now <xref ref-type="bibr" rid="j_forma-2016-0011_ref_010_w2aab2b8b3b1b7b1ab1ac10Aa">[10]</xref>.Of course, we can see some more general applications of some registrations of clusters, essentially not dealing with the notion of an approximation: the notions of an alliance binary relation were not defined in the Mizar Mathematical Library before, and we should think about other properties which are also absent but needed in the context of rough approximations <xref ref-type="bibr" rid="j_forma-2016-0011_ref_009_w2aab2b8b3b1b7b1ab1ab9Aa">[9]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0011_ref_005_w2aab2b8b3b1b7b1ab1ab5Aa">[5]</xref>. Via theory merging, using mechanisms described in <xref ref-type="bibr" rid="j_forma-2016-0011_ref_006_w2aab2b8b3b1b7b1ab1ab6Aa">[6]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0011_ref_007_w2aab2b8b3b1b7b1ab1ab7Aa">[7]</xref>, such elementary constructions can be extended to other frameworks.</abstract>

Rough sets, developed by Zdzisław Pawlak [12], are an important tool to describe the state of incomplete or partially unknown information. In this article, which is essentially the continuation of [8], 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 [11]). Here we drop the classical equivalence- and tolerance-based models of rough sets trying to formalize some parts of [18].The main aim of this Mizar article is to provide a formal counterpart for the rest of the paper of William Zhu [18]. In order to do this, we recall also Theorem 3 from Y.Y. Yao’s paper [17]. The first part of our formalization (covering first seven pages) is contained in [8]. Now we start from page 5003, sec. 3.4. [18]. We formalized almost all numbered items (definitions, propositions, theorems, and corollaries), with the exception of Proposition 7, where we stated our theorem only in terms of singletons. We provided more thorough discussion of the property positive alliance and its connection with seriality and reflexivity (and also transitivity). Examples were not covered as a rule as we tried to construct a more general mechanism of finding appropriate models for approximation spaces in Mizar providing more automatization than it is now [10].Of course, we can see some more general applications of some registrations of clusters, essentially not dealing with the notion of an approximation: the notions of an alliance binary relation were not defined in the Mizar Mathematical Library before, and we should think about other properties which are also absent but needed in the context of rough approximations [9], [5]. Via theory merging, using mechanisms described in [6] and [7], such elementary constructions can be extended to other frameworks.

Binary Relations-based Rough Sets – an Automated Approach

Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok,

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Binary Relations-based Rough Sets \u2013 an Automated Approach"}

Rough sets, developed by Zdzisław Pawlak [12], are an important tool to describe the state of incomplete or partially unknown information. In this article,...

Binary Relations-based Rough Sets – an Automated Approach

Published Online: Dec 08, 2016

Page range: 143 - 155

Received: Feb 15, 2016

DOI: https://doi.org/10.1515/forma-2016-0011

Keywords
rough set, lower approximation, upper approximation, binary relation

© 2016 Adam Grabowski, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Binary Relations-based Rough Sets – an Automated Approach

Published Online: Dec 08, 2016

Page range: 143 - 155

Received: Feb 15, 2016

DOI: https://doi.org/10.1515/forma-2016-0011

Keywordsrough set, lower approximation, upper approximation, binary relation

© 2016 Adam Grabowski, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Keywords
rough set, lower approximation, upper approximation, binary relation