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
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.
NOTATION AND PRELIMINARY DEFINITIONS
Throughout we will be working with a finite propositional language, for some. 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 in the system.
We will use the abbreviations and for classical contradiction and classical tautology respectively. For finite, we will use the abbreviations and to refer to the conjunction and disjunction of all the sentences in respectively. For the next definition and throughout will be classical entailment.
Definition 1. Let. We say that is a probability function on L if the following two conditions hold, for all:
· If then
· If then.
We can restrict probability functions to the set. Such probability functions will be called rational.
A probability distribution on L can be characterized by the values it assigns to the expressions of the form which we call states or worlds, where and stand for p and respectively. We denote the set of states in L by W and define, for as follows: .
We will be assuming that W is an ordered set.
We can characterize by -coordinate vectors in , where
.
Sentences in SL can also be identified with -coordinate vectors. Let and define the -coordinate vector as follows: for each and, if and 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 given is equal to ’, for and . Notice that statements of the form ‘the probability of is equal to’ correspond to the case when .
Let us set, the set of conditional statements in SL. Notice that is, up to classical equivalence, a finite set. For most of this paper we will be interested in the subset.
We will denote the collection of intervals in [0,1] by .
Let us consider and v a map from to. We call v an assignment on and denote the set of such maps by .
We set . For the set of conditionals we will have .
We will sometimes write in compact form; i.e., as, with or, for CADIAG-2 settings, as.
Intervals of the form (i.e., point values) will normally be denoted by itself (so, for example, instead of writing we will write).
Let and. We denote by and the restriction of v on and respectively.
Definition 2. We say that the probability function on L satisfies if, for all, we have that and .
In that sense, we say that is satisfiable or consistent (we use both words interchangeably) if there exists a probability function on L that satisfies.
Definition 3. We say that is a minimal unsatisfiable set (or minimal inconsistent set) if is not satisfiable and, for all, 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 of L is a pair where is a finite non-empty domain and is a map from to [0, 1].
An interpretation is said to be classical if for all. It is said to be rational if for all .
Given an interpretation of, we will refer to the elements in by Latin characters a, b, c…
THE KNOWLEDGE BASE OF CADIAG-2
We can classify CADIAG-2's binary rules () into three different types: rules in which both conditioning and uncertain event are medical entities in (symptom-symptom, ), rules in which both conditioning and uncertain event are medical entities in (disease-disease, ) and those in which the conditioning event is a medical entity in and the uncertain event an entity in (symptom-disease, ). The degree of confirmation in a rule of the first two types is a value in the set and it is in this sense that we say that rules of these types are classical.
The knowledge base of CADIAG- formally contains relationships where the conditioning event is a medical entity in and the uncertain event an entity in . However, such rules are never used by CADIAG-'s inference mechanism and are not taken into account in this paper.
Let be a rule in CADIAG-'s binary knowledge base, with and . The value is intended to quantify the degree to which (the conditioning event) confirms (the uncertain event), claimed in most of the literature on CADIAG- –see, for example, (Adlassnig et al., 1985; Adlassnig et al., 1986) – to have been calculated from a certain database or interpretation as follows:
. (1)
We say in most of the literature. There are some references in which the interpretation suggested for in is different. For example in (Adlassnig, 1986) it is claimed that can be interpreted as a frequency and thus as a probabilistic conditional statement.
Throughout we will use the expression to abbreviate (1). Sometimes, in order to generalize results, we will be considering an interval, say, instead of a single value (i.e., in (1)) and we will be using the expression to abbreviate the corresponding modification of (1). Such modification is motivated by the possibility of alternative, suitable interpretations of the rules in that one could consider interesting in the view of some theoretical or practical aspects. Among these alternative interpretations we consider replacing in equation (1) by the interval (i.e., consider a lower bound for the degrees of confirmation instead of a precise one) or replacing whenever by an interval of the form , for small (i.e., a slightly relaxed interpretation of ).
For the next definition let be an interpretation of and.
Definition 5. We say that is a model of (denoted ) if for all .
Proposition 1. 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 is a rational interpretation such that.
Let be the set given by the values, for. It is assumed that all the values in are rational. Let us consider the minimum common multiple of the denominators of all the elements of, say. We next construct a new interpretation from such that .
We first define from. For each element we set elements in the domain, labeled as follows: . Let us consider now and and assume that. We define on from as follows, for :
It is easy to see that thus defined is such that . ■
For what follows we will be considering the collection of intervals in the set [0, 1]. differs from in that an interval needs to have its maximum and/or minimum in , provided it has a maximum and/or a minimum.
We define the set
and consider for the next proposition.
Proposition 2. If has a model then it has also a rational model.
Proof. Let be an interpretation such that . We then have that, for all , .
For each we consider the inequalities
where is assumed to be of the form (for of any other form we replace '<' in the inequalities above by '' as required) and with min replaced by or accordingly.
Let us also consider, for each, the inequalities
and, for greater than , the inequality (the inequality otherwise).
The solution set of the linear system above with unknown values, is not empty, since is assumed to be a solution, and needs to contain rational solutions due to the form of the intervals in. Therefore, there has to exist a rational interpretation of that satisfies. ■