@MISC{ROUGHS_3.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Binary Relations-Based Rough Sets -- An Automated Approach},
  SECTION1 = {Preliminaries},
  SECTION2 = {On the Union and the Intersection of Two Relational Structures},
  SECTION3 = {Ordinary Properties of Maps},
  SECTION4 = {On the Relational Structure Generated by Rough Approximation},
  SECTION5 = {Construction Revisited: Yao's Theorem 3},
  SECTION6 = {Transitive Binary Relations},
  SECTION7 = {Mediate and Transitive Binary Relations},
  SECTION8 = {Alliance Binary Relations},
  SECTION9 = {Preparation for Translation of Proposition 10 (7H')},
  SECTION10 = {Translation Continued},
  SECTION11 = {On the Uniqueness of Binary Relations to Generate Rough Sets},
  DAY = {15},
  MONTH = {February},
  YEAR = {2016},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio\l kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {Rough sets, developed by Pawlak, are important tool to
  describe situation of incomplete or partially unknown information.
  In this article, which is essentially the continuation of
  \cite{ROUGHS_2.ABS}, 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 Mathematica Library).
  Here we drop the classical equivalence- and tolerance-based models
  of rough sets trying to formalize some parts of
  \cite{Zhu:2007}.
  \par
   The main aim of this Mizar article is to provide a formal counterpart
   for the rest of the paper of William Zhu.
   In order to do this, we recall also Theorem 3 from Y.Y. Yao's
   paper.
  The first part of our formalization (covering first seven pages)
  is contained in \cite{ROUGHS_2.ABS}.
   Now we start from page 5003, sec. 3.4.
   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 "\verb!positive_alliance!"
   and its connection with seriality and reflexivity (and also transitivity).
   Examples were not covered as a rule as we aim to provide a more
  general mechanism of finding appropriate models for approximation
  spaces in Mizar providing more automatization than it is now.
  \par
  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 was  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.}}

@ARTICLE{Zhu:2007,
 AUTHOR = {Zhu, William},
 TITLE = {Generalized Rough Sets Based on Relations},
 JOURNAL = {Information Sciences},
 VOLUME = 177,
 PAGES = {4997--5011},
 YEAR=2007}





