Automated Comparative Study of Some Generalized Rough Approximations

Issue title: Concurrency, Specification, and Programming: Special Issue of Selected Papers of CS&P 2018

Guest editors: H. Schlingloff and W. Penczek

Article type: Research Article

Authors: Grabowski, Adam^{; *}

Affiliations: Institute of Informatics, University of Białystok, Konstantego Ciołkowskiego 1M, 15-245 Białystok, Poland. adam@math.uwb.edu.pl

Correspondence: [*] Address for correspondence: Institute of Informatics, University of Białystok, Konstantego Ciołkowskiego 1M, 15-245 Białystok, Poland.

Abstract: The paper contains some remarks on building automated counterpart of a comparison of some generalized rough approximations of sets, where the classical indiscernibility relation is generalized to arbitrary binary relation. Our focus was on translating rationality postulates for such operators by means of the Mizar system – the software and the database which allows for expressing and checking mathematical knowledge for the logical correctness. The main objective was the formal (and machine-checked) proof of Theorem 4.1 from A. Gomolińska’s paper “A Comparative Study of Some Generalized Rough Approximations”, hence the present title. We provide also the discussion on how to make the presentation more efficient to reuse the reasoning techniques of the Mizar verifier.

Keywords: rough approximation, formalization of mathematics, Mizar Mathematical Library

DOI: 10.3233/FI-2021-2019

Journal: Fundamenta Informaticae, vol. 179, no. 2, pp. 165-182, 2021