PROVING (automatically and certainly)
THE UNCERTAIN (rough and almost impossible)
Anita Wasilewska (Stony Brook) and Laurent Vigneron (Stony Brook and INRIA (France))
The theory of rough sets is a relatively new research direction concerned with analysis and modeling of classification and decision problems involving vague, imprecise, uncertain, or incomplete information. It gave rise to new formal approaches to approximate reasoning, digital logic analysis and reduction, control algorithm aquisition, machine learning algorithms, pattern recognition, medical and neural networks applications and lately, knowledge discovery or data base mining.
We will show that a notion of rough equality of sets leads to a definition of a new class of algebras, called rough-quasi S5 and S4 algebras. These algebras are quasi-Boolean version of topological S4 and S5 Boolean algebras which are algebraic models for modal logics S5 and S4, respectively.
We have used a theorem prover DATAC (Déduction Automatique dans des Théories Associatives et Commutatives) developed at CRIN & INRIA Lorraine, Nancy (France) by the second author to examine their properties. We will discuss here the prover and some the most interesting properties of the RQ4 and RQ5 algebras, which were chosen from over seven hundred which were discovered and proved automatically by a theorem prover DATAC .