Information Technology Reference
In-Depth Information
relations. An axiomatic system of the logic LNIS is presented in Section 3, and
corresponding soundness and completeness theorems are proved. The decidabil-
ity of the logic is proved in Section 4. In Section 5, it is shown that the current
work can be extended to other types of relations defined on NISs as well. Section
6 concludes the article.
2 Logic for Non-deterministic Information Systems
In this section, we shall propose a logic LNIS (logic for non-deterministic infor-
mation systems) which can be used to reason about the rough set approximations
with respect to indiscernibility, similarity and inclusion relations induced from
NISs. Moreover, it can also talk about the attributes, attribute-values of the
objects.
2.1 Syntax
The language
L
of LNIS contains (i) a non-empty finite set
A
of attribute con-
stants, (ii) for each
a
V
a
of attribute-value constants,
(iii) a non-empty countable set
PV
of propositional variables, and (iv) the propo-
sitional constants
∈A
, a non-empty finite set
.
The atomic well-formed formulae (wffs) are the propositional variables
p
from
PV, and the tuples of the form (
a, v
)where
a
,
↥
∈V
a
. The tuples (
a, v
)
are called
descriptors
[18]. The set of all descriptors will be denoted by
∈A
and
v
D
.
¬
∧
Using the atomic wffs, Boolean connectives
(negation),
(conjunction),
and the modal operators
1
B
,
2
B
and
3
B
for each
B ↆA
,thewffsof
L
are
then defined recursively as:
1
B
ʱ
2
B
ʱ
3
B
ʱ.
ʱ
::=
p
|
(
a, v
)
|¬
ʱ
|
ʱ
∧
ʲ
|
|
|
k
{a}
a
. Derived connectives
For
a
∈A
, we shall simply write
,
k
∈{
1
,
2
,
3
}
,as
1
B
,
2
B
,
3
B
(diamonds).
are the usual ones:
∨
(disjunction),
→
(implication),
♦
♦
♦
We shall use the same symbol
L
to denote the set of all wffs of the language
L
.
2.2 Semantics
As we desired, the semantics of
will be based on NISs. Thus we have the
following definition of models. Recall that for an equivalence relation
R
on
U
,
and for
x
L
∈
U
,[
x
]
R
denotes the equivalence class of
x
with respect to
R
.
Definition 2.
Amodelof
L
is defined as a tuple
M
S
,V
)
,where
S
:= (
:=
,
a∈A
V
a
,F
)
is a non-deterministic information system, and V
:
PV
(
W,
A
→
2
W
is a valuation function.
,
a∈A
V
a
,
The satisfiability of a wff
ʱ
in a model
M
:= (
S
,V
), where
S
:= (
W,
A
F
), at an object
w
=
ʱ
,isdefinedasfollows.Weomit
the cases of propositional constants and Boolean connectives.
∈
W
, denoted as
M
,w
|
