Formalizing lattice-theoretical aspects of rough and fuzzy sets

Abstract

Fuzzy sets and rough sets are well-known approaches to incomplete or imprecise data. In the paper we briefly report how these frameworks were successfully encoded with the help of one of the leading computer proof assistants in the world. Even though fuzzy sets are much closer to the set theory implemented within the Mizar library than rough sets, lattices as a basic viewpoint appeared a very feasible one. We focus on the lattice-theoretical aspects of rough and fuzzy sets to enable the application of external theorem provers like EQP or Prover9 as well as to translate them into TPTP format widely recognized in the world of automated proof search. The paper is illustrated with the examples taken just from one of the largest repositories of computer-checked mathematical knowledge – the Mizar Mathematical Library. Our formal development allows both for further generalizations, building on top of the existing knowledge, and even merging of these approaches.