Rough sets based proofs visualisation

We present here an approach we used for proving important properties of clopen topological spaces. We combine powerful theorem provers techniques (and implementations) with a graphical technique based on a graphical representation of a rough set, called rough diagrams. Rough diagrams are a generalization of a classical notion of Venn Diagrams for algebra of sets to clopen topological spaces. We use them as a powerful automated technique of constructing counter-models of properties the prover has a hard time proving and the user might suspect of being false. It means we propose to add a visual tool to a prover that after some fixed number of prover deductions would start constructing a visual counter-model for a property the prover is trying to prove. A prover with the visual tool is called a visual prover. The visual prover has a completeness property: for any rough set equality we can construct its proof or its counter-model