Information Technology Reference
In-Depth Information
Let
T
=(
Φ
,
R
)
be a theory of
CadL
. We have the following rules:
•
Reflexivity rule
(
φ
,
η
)
∈
Φ
T
(
φ
,
η
)
(
REF
)
•
Evaluation rules
T
(
φ
,
η
)
T
(
θ
,
ζ
)
(
AND
)
T
(
φ
∧
θ
,
min
(
η
,
ζ
))
T
(
φ
,
η
)
T
(
θ
,
ζ
)
T
(
φ
∨
θ
,
(
OR
)
max
(
η
,
ζ
))
T
(
φ
,
η
)
T
(
∼
φ
,
(
NOT
)
−
η
)
1
•
Manipulation rules
R
c
θ
,
φ
,
η
∈
T
(
θ
,
ζ
)
(
C
)
for
ζ
>
0
T
(
φ
,
min
(
η
,
ζ
))
R
me
θ
,
φ
,
0
∈
T
(
θ
,
1
)
(
ME
)
T
(
φ
,
0
)
R
ao
θ
,
φ
,
1
∈
T
(
φ
,
0
)
(
)
AO
T
(
θ
,
0
)
REF
simply aims at formalizing for general theories of the form
(
Φ
,
R
)
that a
graded statement that belongs to
(i.e., to the input in CADIAG2) is itself inferred
as a consequence (i.e., as part of the output in CADIAG2). The evaluation rules
AND
Φ
OR
and
NOT
aim at formalizing the assignments to compound medical enti-
ties along the inference process in a run of the inference mechanism of CADIAG2
and the rules
C
,
ME
and
AO
correspond to the use of rules of type
c
,
me
and
ao
respectively during the inference process, as explained in the previous section.
Given a theory
,
T
of
CadL
and a graded statement
(
φ
,
η
)
,a
proof
of
(
φ
,
η
)
from
T
in
CadL
is defined as a finite sequence of
sequents
of the form
T
(
φ
,
η
)
, ...,T
(
φ
,
η
)
1
1
n
n
with
(
φ
,
η
)=(
φ
,
η
)
and where, for
i
∈{
1
, ...,
n
}
, each
(
φ
,
η
)
in
T
(
φ
,
η
)
n
n
i
i
i
i
follows from
by the application of one of the rules above, from graded statements
in previous sequents.
We say that there exists a
maximal proof
of
T
(
φ
,
η
)
from
T
in
CadL
if there
exists a proof of
(
φ
,
η
)
from
T
and there is no proof from
T
of
(
φ
,
ζ
)
with
η
≺
ζ
.
Let us now consider the theory
T
=(
Φ
,
R
)
, with
R
=
KR
,
φ
a diagnose in
L
and
η
∈
[
. As should be clear from the description of the inference mechanism of
CADIAG2 given in Section 22.3, the medical entity
0
,
1
]
φ
along with the value
η
would
