Formal Development of Rough Inclusion Functions
Adam Grabowski · Formalized Mathematics · 2019
Summary Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article, continuing the formalization of rough sets [12], we give the formal characterization of three rough inclusion functions (RIFs). We start with the standard one, κ £ , connected with Łukasiewicz [14], and extend this research for two additional RIFs: κ 1 , and κ 2 , following a paper by Gomolińska [4], [3]. We also define q-RIFs and weak q-RIFs [2]. The paper establishes a formal counterpart of [7] and makes a preliminary step towards rough mereology [16], [17] in Mizar [13].