Information Technology Reference
In-Depth Information
inference mechanism can depend on the order in which the rules are applied. Such
a drawback is easily avoided by assuming (as we do for this paper) that the chosen
value, the maximal among all those produced along the inference with respect to the
partial ordering
, is only computed at the end of the process.
Notice that the system can generate what is called a
runtime inconsistency
given
the ordering
, produced when both values 0 and 1 are assigned to a medical entity
along the inference process. In such case the system stops and produces an error
message.
22.4
A Formalization of the Inference Process
In this section we provide a logical formalization of the inference process in CA-
DIAG2 by means of a complete set of rules aimed at describing the possible steps
along the inference.
Let
L
be a finite propositional language and
SL
the set of sentences obtained
from
L
as its closure under conjunction (
∧
), disjunction (
∨
) and negation (
∼
). In
{
,...,
p
l
}
the context of CADIAG2, the set
of basic medical entities will be a
subset of
L
and the compound medical entities that can be obtained from
L
will be
a subset of
SL
.
Let
p
1
Γ
=
{
φ
1
, ...,
φ
n
}⊂
SL
,forsome
n
∈
N
. We will denote the sentence
φ
1
∧... ∧
φ
n
by
Γ
.
Definition 29.
A graded statement in L is a pair of the form
(
φ
,
η
)
, with
φ
∈
SL and
η
∈
[
0
,
1
]
.
In the context of CADIAG2 a graded statement of the form
(
φ
,
η
)
represents the
medical entity
φ
together with the value assigned to it,
η
, either at the outset (i.e., if
φ
is part of the initial information with which CADIAG2 gets started) or during the
inference process.
22.4.1
The Calculus CadL
In this subsection we summarize results in [6] and present, in a slightly simpli-
fied version, the calculus
CadL
aimed at formalizing the inference process in
CADIAG2.
First we define the notion of theory of
CadL
:
Definition 30.
A theory
T
of
CadL
is a pair of the form
(
Φ
,
R
)
characterized as
follows:
•
Φ
is a finite set of graded statements in L.
R
ao
, with R
c
,R
me
and R
ao
finite collections of rules of type
c
,
me
and
ao
respectively.
R
c
R
me
•
R
=
∪
∪
In the context of CADIAG2
would be given by the input of the system (i.e., the
initial information about the patient) and
R
would be given by
KR
.
Φ
