Title Here - Logic



The consistency of the medical expert system CADIAG-2: A probabilistic approach

Pavel Klinov, Bijan Parsia and David Picado Muiño

The University of Manchester

Oxford Road, Manchester M13 9PL, UK

[pklinov|bparsia]@cs.man.ac.uk

Institut für Diskrete Mathematik und Geometrie

Wiedner Hauptstrasse 8. A-1040 Vienna, Austria

picado@logic.at

ABSTRACT

CADIAG-2 is a well known rule-based medical expert system aimed at providing support in medical diagnose in the field of internal medicine. Its knowledge base consists of a large collection of IF-THEN rules that represent uncertain relationships between distinct medical entities. Given this uncertainty and the size of the system it has been challenging to validate its consistency. Recent attempts to partially formalize CADIAG-2's knowledge base into decidable Gödel logics have shown that, on that formalization, the system is inconsistent. In this paper we adopt an alternative, more expressive formalization of CADIAG-2’s knowledge base as a set of probabilistic conditional statements and apply our state-of-the-art probabilistic logic solver (Pronto) to confirm its inconsistency and to compute all its conflicting sets of rules under a slightly relaxed interpretation of them. Once this is achieved, we define a measure to evaluate inconsistency and discuss suitable repair strategies for CADIAG-2 and similar systems.

Keywords: CADIAG-2, inconsistency, measures of inconsistency, probabilistic satisfiability, Pronto, repairing inconsistency, rule-based expert systems.

Introduction

CADIAG-2 (Computer Assisted DIAGnosis) is a well known rule-based expert system aimed at providing support in diagnostic decision making in the field of internal medicine. Its design and construction was initiated in the early 80's at the Medical University of Vienna by K.P. Adlassnig –see (Adlassnig et al., 1986; Adlassnig et al., 1985; Adlassnig, 1986; Leitich et al., 2002) for more on the origins and design of CADIAG-2–.

CADIAG-2 consists of two fundamental pieces: the inference engine and the knowledge base. The inference engine –see (Ciabattoni et al., 2010; Picado Muiño, 2010) for alternative formalizations and analyses of CADIAG-2's inference– is based on methods of approximate reasoning in fuzzy set theory, in the sense of (Zadeh, 1965; Zadeh, 1975). In fact CADIAG-2 is presented in some monographs as an example of a fuzzy expert system –see for example (Klir et al., 1988; Zimmermann, 1991)–.

The knowledge base consists of a set of IF-THEN rules –also known in the literature as production rules– intended to represent relationships between distinct medical entities: symptoms, findings, signs and test results (S) on the one hand and diseases and therapies (D) on the other. The vast majority of them are binary (i.e., they relate single medical entities) and only such rules are considered in this paper. The one that follows is an example of a binary rule of CADIAG-2, taken from (Adlassnig et al., 1986):

IF suspicion of liver metastases by liver palpation

THEN pancreatic cancer

with degree of confirmation 0.3

The degree of confirmation refers, intuitively, to the degree to which the conditioning event (i.e., ‘suspicion of liver metastases by liver palpation’ in the example above) confirms the uncertain event (i.e., ‘pancreatic cancer’ above). How these degrees of confirmation are to be formally interpreted will be discussed later.

In this paper we present a formalization of a coded version of the binary fragment of CADIAG-2's knowledge base (i.e., that contains only codes for the identification of the distinct medical entities) as a probabilistic logic theory. We then check the satisfiability of that formalization with Pronto, our probabilistic description logic solver, which we briefly introduce. We find that CADIAG-2 is highly unsatisfiable (confirming the results of an alternative, weaker formalization, (Ciabattoni et al., 2010)) and analyze the sources of unsatisfiability.

To our knowledge, the probabilistic version of CADIAG-2 is the largest PSAT (Probabilistic SATisfiability) problem to be solved by an automated reasoner and is certainly the largest non-artificial one. This is, perhaps, a bit misleading as it is comparatively easy to detect unsatisfiability by first heuristically detecting small but likely unsatisfiable fragments and then performing a satisfiability check on each fragment. While this might suffice to validate that CADIAG-2 is unsatisfiable it is not sufficient, without further qualification, to detect all conflicting sets of rules, nor can it ensure that a satisfiable fragment is so in the context of the entire knowledge base.

As CADIAG-2 is too large (the number of rules in the binary fragment we are concerned with is over 18000) we describe an approach to split the knowledge base into comparatively large fragments that can be tested independently and prove that such methodology is complete, i.e., is guaranteed to find all conflict sets. With this methodology we are able to determine that CADIAG-2 contains numerous sets of conflicting rules and compute all of them for a slightly relaxed interpretation of the knowledge base.

We complete the paper with the introduction of an inconsistency measure aimed at evaluating CADIAG-2-like databases and a brief account of suitable repair strategies for CADIAG-2 and similar systems. The measure presented attempts to quantify how far the knowledge base is from consistency and its computation, in as much as it yields an adjustment in the degree of confirmation or uncertainty of each conditional statement, provides the modeler with a possible repair of the database.

[pic]

NOTATION AND PRELIMINARY DEFINITIONS

Throughout we will be working with a finite propositional language[pic], for some[pic]. We will denote by SL its closure under Boolean connectives. Within the context of CADIAG-2 the language L will represent the set of medical entities [pic] in the system.

We will use the abbreviations [pic] and [pic]for classical contradiction and classical tautology respectively. For [pic] finite, we will use the abbreviations [pic] and [pic] to refer to the conjunction and disjunction of all the sentences in [pic] respectively. For the next definition and throughout [pic] will be classical entailment.

Definition 1. Let[pic]. We say that [pic] is a probability function on L if the following two conditions hold, for all[pic]:

• If [pic] then [pic]

• If [pic] then[pic].

We can restrict probability functions to the set[pic]. Such probability functions will be called rational.

A probability distribution [pic] on L can be characterized by the values it assigns to the expressions of the form [pic] which we call states or worlds, where [pic] and [pic] stand for p and [pic] respectively. We denote the set of states in L by W and define, for [pic] [pic] as follows: [pic].

We will be assuming that W is an ordered set.

We can characterize [pic] by [pic]-coordinate vectors in [pic], where

[pic].

Sentences in SL can also be identified with [pic]-coordinate vectors. Let [pic] and define the [pic]-coordinate vector [pic] as follows: for each [pic] and[pic], [pic] if [pic] and [pic] otherwise.

We define probability on conditional statements in SL from the notion of unconditional probability in the conventional way.

We will be dealing with conditional probabilistic statements of the form ‘the probability of [pic] given [pic] is equal to [pic]’, for [pic] and [pic]. Notice that statements of the form ‘the probability of [pic] is equal to[pic]’ correspond to the case when [pic].

Let us set[pic], the set of conditional statements in SL. Notice that [pic] is, up to classical equivalence, a finite set. For most of this paper we will be interested in the subset[pic].

We will denote the collection of intervals in [0,1] by [pic].

Let us consider [pic] and v a map from [pic] to[pic]. We call v an assignment on [pic] and denote the set of such maps by [pic].

We set [pic]. For the set of conditionals [pic] we will have [pic].

We will sometimes write [pic] in compact form; i.e., as[pic], with [pic] or, for CADIAG-2 settings, as[pic].

Intervals of the form [pic] (i.e., point values) will normally be denoted by [pic] itself (so, for example, instead of writing [pic] we will write[pic]).

Let [pic] and[pic]. We denote by [pic] and [pic]the restriction of v on [pic] and [pic] respectively.

Definition 2. We say that the probability function [pic] on L satisfies [pic] if, for all[pic], we have that [pic] and [pic].

In that sense, we say that [pic] is satisfiable or consistent (we use both words interchangeably) if there exists a probability function [pic] on L that satisfies[pic].

Definition 3. We say that [pic] is a minimal unsatisfiable set (or minimal inconsistent set) if [pic] is not satisfiable and, for all[pic], [pic] is satisfiable.

The words ‘satisfiable’ and ‘consistent’ will be used interchangeably throughout this paper.

In order to prove some results and characterize the meaning of degree of consistency in CADIAG-2 we will regard L as a collection of unary predicates or sets in a first-order language and SL the closure of predicates in L under boolean combinations.

Definition 4. An interpretation [pic] of L is a pair [pic] where [pic] is a finite non-empty domain and [pic] is a map from [pic] to [0, 1].

An interpretation [pic] is said to be classical if [pic] for all[pic]. It is said to be rational if [pic] for all [pic].

Given an interpretation [pic] of[pic], we will refer to the elements in [pic] by Latin characters a, b, c…

THE KNOWLEDGE BASE OF CADIAG-2

We can classify CADIAG-2's binary rules ([pic]) into three different types: rules in which both conditioning and uncertain event are medical entities in [pic] (symptom-symptom, [pic]), rules in which both conditioning and uncertain event are medical entities in [pic] (disease-disease, [pic]) and those in which the conditioning event is a medical entity in [pic] and the uncertain event an entity in [pic] (symptom-disease, [pic]). The degree of confirmation in a rule of the first two types is a value in the set [pic] and it is in this sense that we say that rules of these types are classical.

The knowledge base of CADIAG-[pic] formally contains relationships where the conditioning event is a medical entity in [pic] and the uncertain event an entity in [pic]. However, such rules are never used by CADIAG-[pic]'s inference mechanism and are not taken into account in this paper.

Let [pic] be a rule in CADIAG-[pic]'s binary knowledge base, with [pic] and [pic]. The value [pic] is intended to quantify the degree to which [pic] (the conditioning event) confirms [pic] (the uncertain event), claimed in most of the literature on CADIAG-[pic] –see, for example, (Adlassnig et al., 1985; Adlassnig et al., 1986) – to have been calculated from a certain database or interpretation [pic] as follows:

[pic]. (1)

We say in most of the literature. There are some references in which the interpretation suggested for [pic] in [pic] is different. For example in (Adlassnig, 1986) it is claimed that [pic] can be interpreted as a frequency and thus [pic] as a probabilistic conditional statement.

Throughout we will use the expression [pic] to abbreviate (1). Sometimes, in order to generalize results, we will be considering an interval, say[pic], instead of a single value (i.e., [pic] in (1)) and we will be using the expression [pic] to abbreviate the corresponding modification of (1). Such modification is motivated by the possibility of alternative, suitable interpretations of the rules in [pic] that one could consider interesting in the view of some theoretical or practical aspects. Among these alternative interpretations we consider replacing [pic] in equation (1) by the interval [pic] (i.e., consider [pic] a lower bound for the degrees of confirmation instead of a precise one) or replacing [pic] whenever [pic] by an interval of the form [pic], for [pic] small (i.e., a slightly relaxed interpretation of [pic]).

For the next definition let [pic] be an interpretation of [pic] and[pic].

Definition 5. We say that [pic] is a model of [pic] (denoted [pic]) if [pic] for all [pic].

Proposition 1. [pic] has a classical model if and only if it has a rational model.

Proof. The right implication follows trivially from the fact that every classical interpretation is also rational. In order to prove the left implication let us assume that [pic] is a rational interpretation such that[pic].

Let [pic] be the set given by the values[pic], for[pic]. It is assumed that all the values in [pic] are rational. Let us consider the minimum common multiple of the denominators of all the elements of[pic], say[pic]. We next construct a new interpretation [pic] from [pic] such that [pic].

We first define [pic] from[pic]. For each element [pic] we set [pic] elements in the domain[pic], labeled as follows: [pic]. Let us consider now [pic] and [pic] and assume that[pic]. We define [pic] on [pic] from [pic] as follows, for [pic]:

[pic] [pic]

It is easy to see that [pic] thus defined is such that [pic]. ■

For what follows we will be considering the collection of intervals [pic] in the set [0, 1]. [pic] differs from [pic] in that an interval [pic] needs to have its maximum and/or minimum in [pic], provided it has a maximum and/or a minimum.

We define the set

[pic]

and consider [pic] for the next proposition.

Proposition 2. If [pic] has a model then it has also a rational model.

Proof. Let [pic] be an interpretation such that [pic]. We then have that, for all [pic], [pic].

For each [pic] we consider the inequalities

[pic]

where [pic] is assumed to be of the form [pic] (for [pic] of any other form we replace ' ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download