Skip to Main content Skip to Navigation
Book sections

Rough Algebras & Automated Deduction

Anita Wasilewska 1 Laurent Vigneron 2
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The notion of rough equality was introduced by Pawlak in 1982, and has been extensively examined over the years. The rough R5 and R4 algebras investigated here are particular cases of topological rough algebras introduced by Anita Wasilewska. We examine and discuss here some of their most interesting properties, their relationship with each other, and with the topological Boolean S4 and S5 algebras, which are algebraic models for modal logics S4 and S5, respectively. The presented properties were chosen out of over seven hundred theorems which were discovered and proved automatically by the theorem prover daTac (Déduction Automatique dans des Théories Associatives et Commutatives). This prover was developed at LORIA, Nancy (France), by the second author.
Document type :
Book sections
Complete list of metadatas
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:01:54 PM
Last modification on : Wednesday, August 7, 2019 - 12:18:08 PM


  • HAL Id : inria-00098475, version 1



Anita Wasilewska, Laurent Vigneron. Rough Algebras & Automated Deduction. L. Polkowski & A. Skowron. Rough Sets in Knowledge Discovery, Springer Verlag, pp.261-275, 1998. ⟨inria-00098475⟩



Record views