On the computer-assisted reasoning about rough sets

Abstract

The paper presents some of the issues concerning a formal description of rough sets. We require the indiscemibility relation to be a tolerance of the carrier, not an equivalence relation, as in the Pawlak's classical approach. As a tool for formalization we use the Mizar system, which is equipped with the largest formalized library of mathematical facts. This uniform and computer-checked for correctness framework seems to present a satisfactory level of generality and may be used by other systems as well as it is easily readable for humans.© Springer-Verlag Berlin Heidelberg 2005.