Noname manuscript No. (will be inserted by the editor) A probabilistic interpretation of the medical expert system CADIAG-2 David Picado Muiño Received: date / Accepted: date Abstract CADIAG-2 is a well known expert system aimed at providing support for medical diagnose in the field of internal medicine. CADIAG-2 consists of a knowl- edge base in the form of a set of IF-THEN rules that relate distinct medical entities, in this paper interpreted as conditional probabilistic statements, and an inference engine constructed upon methods of fuzzy set theory. The aim underlying this paper is the understanding of the logical structure of the inference in CADIAG-2. To that purpose we provide a (probabilistic) logical for- malisation of the inference of the system and check its adequacy with probabilistic logic. Keywords Knowledge-based systems · rule-based expert systems · fuzzy expert systems · probabilistic inference · CADIAG-2 1 Introduction CADIAG-2 (Computer Assisted DIAGnosis) is a well known rule-based expert system that aims at pro- viding 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) or (Leitich et al., 2002) for more on the origins and de- sign of CADIAG-2–. CADIAG-2 consists of two fundamental pieces: the inference engine and the knowledge base. The inference Institut für Diskrete Mathematik und Geometrie Wiedner Hauptstrasse 8 1040 Vienna, Austria Tel.: +43-1-58801-10427 Fax: +43-1-58801-910427 E-mail: david.muino@tuwien.ac.at engine is based on methods of approximate reasoning in fuzzy set theory, in the sense of (Zadeh, 1965) and (Zadeh, 1975). In fact CADIAG-2 is presented in some monographs as an example of a fuzzy expert system, for example in (Klir and Folger, 1988) or (Zimmer- mann, 1991). The knowledge base consists of a set of IF-THEN rules, also known as production rules in the literature, intended to represent relationships between distinct medical entities: symptoms, findings, signs and test results on the one hand and diseases and thera- pies on the other. The number of rules in the knowl- edge base of CADIAG-2 is approximately 40.000. The vast majority of them are binary (i.e., they relate single medical entities) and only such rules are considered in this paper. The rules in CADIAG-2 are defined along with a certain degree of confirmation which intuitively expresses the degree to which the antecedent confirms the consequent. For example, IF suspicion of liver metastases by palpation THEN pancreatic cancer with degree of confirmation 0.3 We can identify such degrees of confirmation with probabilities and the rules themselves with conditional probabilistic statements. In (Adlassnig, 1986) it is stated that degrees of confirmation can be interpreted as fre- quencies and, more generally, as probabilities. An in- terpretation in terms of degrees of belief of the doctor (or doctors) on the truth of the consequent given that the antecedent of the rule holds is also possible. This fact motivates a probabilistic interpretation of the infer- ence in CADIAG-2 and leads to the primary aim of this paper: formalise the inference in CADIAG-2 on proba- bilistic grounds and check its adequacy with probabil- ity logic –see (Halpern, 2003)– or, more generally, with probability theory. We shall not expect big surprises in 2 this respect. The inference mechanism in CADIAG-2 proceeds in a compositional way and thus it is bound to be probabilistically unsound (as will be clarified later). This was soon observed in earlier studies concerning the celebrated expert system MYCIN –see (Buchanan and Shortliffe, 1984) or (Shortliffe, 1976) for a description of MYCIN and (Hajek, 1988), (Hajek, 1989), (Hajek and Valdés, 1994), (Heckerman, 1986), (Valdés, 1992) for probabilistic approaches to it–. How far the inference mechanism of CADIAG-2 is from probabilistic sound- ness remains to be seen though. It is worth mentioning here that, although the inter- est among theoretical AI researchers in rule-based ex- pert systems seems to be lesser today than some years ago, rule-based expert systems are very popular among AI engineers. Many CADIAG-2-like systems are in use and more are being built for future implementation. It is mainly for this reason that we believe that further analysis and understanding of CADIAG-2-like systems is of relevance. This paper is in some way a continuation of (Cia- battoni and Vetterlein, 2009). In (Ciabattoni and Vet- terlein, 2009) the inference in CADIAG-2 is formalised by means of a logical calculus, CadL, and compared to t-norm-based formalisms –see (Hajek, 1998)–. It is shown that CadL does not respond to any t-norm-based (or to any fragment of a t-norm-based) logic. As far as we know (Ciabattoni and Vetterlein, 2009) consti- tutes the first attempt at formalising and understand- ing CADIAG-2 in a logical way. The present paper is the second. This paper is structured as follows. In Section 2 we give some basic definitions and introduce most of the notation used later in the other sections. In Section 3 the inference process in CADIAG-2 is described when restricted to the binary rules of its knowledge base. In Section 4 the formal system CadPL is defined and anal- ysed in the light of probability logic. CadPL is a for- malisation of the inference mechanism of CADIAG-2 based on a probabilistic interpretation of it. 2 PRELIMINARY DEFINITIONS AND NOTATION Throughout we will be working with a finite propo- sitional language L = {p1, ...,pn}, for some n ∈ N. We will denote by SL its closure under classical connec- tives. Within the context of CADIAG-2 the language L will represent the set of medical entities occurring in the system. By S ⊂ L we will denote the set of symptoms, findings, signs and test results (symptoms for short) and by D ⊂ L the set of diseases and therapies (diseases for short). Let us set LLit = {p ,¬p | p ∈ L} ⊂ SL, the set of literals of the language L. Consider ∆ = {φ1, ...,φk} ⊆ SL, for some k ∈ N. We will denote by ∧ ∆ the sentence φ1 ∧ ...∧φk. Definition 1 Let ω : SL −→ [0, 1]. We say that ω is a probability function on L if the following two conditions hold, for all θ,φ ∈ SL: – If |= θ then ω(θ) = 1. – If |= ¬(θ ∧φ) then ω(θ ∨φ) = ω(θ) + ω(φ).1 We define probability on conditional events in the conventional way. For ω a probability function on L and φ,θ ∈ SL, ω(φ|θ) = ω(φ∧θ) ω(θ) . Notice that if ω(θ) = 0 then ω(φ|θ) is not defined. We are interested in knowledge bases (CADIAG-2- like knowledge bases) that consist of finite collections of IF-THEN rules. We will identify such rules with triples of the form 〈θ,φ,η〉, where θ ∈ SL is the antecedent (or, more in keeping with probabilistic terminology, the conditioning event), φ ∈ SL is the consequent (or the uncertain event) and η ∈ [0, 1] is the degree to which θ confirms φ, which we will interpret as the conditional probability of φ given θ. Let K = {〈θ,φ,η〉 | θ,φ ∈ SL, η ∈ [0, 1]} be the set of all such triples in the language L. For the next two definitions let Φ ⊂K. Definition 2 We say that a probability function ω on L (probabilistically) satisfies Φ if, for all 〈θ,φ,η〉 ∈ Φ, we have that ω(θ) > 0 and ω(φ|θ) = η. Definition 3 We say that Φ is satisfiable (or consis- tent) if there exists a probability function ω on L that satisfies Φ.2 Next we define a partial ordering relation relevant in the context of the inference mechanism of CADIAG-2. Definition 4 Let � be the partial ordering relation on [0, 1] defined as follows: for a,b ∈ [0, 1], a � b if and only if 0 < a ≤ b or 0 ≤ a < 1 and b = 0. We define the strict partial ordering ≺ from � in the conventional way. As we will see later, the definition of the ordering � responds to the use of both 0 and 1 as maximal values in 1 Here (and throughout) |= represents classical entailment. 2 We will be using the terms ’satisfiable’ and ’consistent’ indis- tinguishably. 3 CADIAG-2. The value 0 denotes certainty in the non- occurrence of an event or falsity of a statement and the value 1 denotes certainty in its occurrence or its truth. For the next definition let D = [0, 1] × [0, 1] −{(0, 1), (1, 0)}. Definition 5 The function max∗ : D −→ R is defined as follows, for (a,b) ∈ D: max∗(a,b) = { a if b ≺ a b otherwise The definition of max∗ is extended to more than two arguments in its trivial way. 3 THE INFERENCE IN CADIAG-2 In this section we briefly describe the inference mechanism in CADIAG-2 when restricted to the set of binary rules, which from now we will denote by ΦCB. A more detailed description can be found in (Ciabattoni and Vetterlein, 2009). We have three different types of rules in ΦCB accord- ing to the typology defined in (Ciabattoni and Vetter- lein, 2009): – Type confirming to the degree d (c). A rule of this type is formalised in our settings as 〈φ,p,η〉 for p ∈ L, φ ∈ LLit and η ∈ (0, 1]. The one that follows is an example of a rule of this type in ΦCB: IF suspicion of pancreatic tumor by comput- erized tomography THEN pancreatic cancer with degree of confirmation 0.85 – Type mutually exclusive (me). A rule of type me is formalised as 〈q,¬p, 1〉, for p,q ∈ L. We give an example of a rule of this type: IF positive rheumatoid factor THEN not seronegative rheumatoid arthritis with degree of confirmation 1 – Type always occurring (ao). A rule of type ao is formalised as 〈¬q,¬p, 1〉, for p,q ∈ L. What follows is an example of a rule of this type in ΦCB: IF not chorea minor THEN not polymyositis with degree of confirmation 1 The types me and ao are classical in the sense that the degree of confirmation for the rules of these types is 1 and that the antecedent of such rules (or evidence in our settings) needs to be confirmed (it needs to be given value 1 by the system, see below) in order for these rules to be triggered by the inference engine. We will denote by Φc, Φme and Φao the subsets of ΦCB containing the rules of types c, me and ao respec- tively. The inference engine in CADIAG-2 gets started with a set of symptoms and diseases occurring in ΦCB present in the patient. Let Γ ⊂ L be the set of such medical entities. CADIAG-2 starts with an assignment v0 on Γ that gives a value in the interval [0, 1] to each entity in Γ. The values assigned by v0 are, according to most of the literature on CADIAG-2, intended to stand for mem- bership degrees in the context of fuzzy set theory and represent the degrees to which such entities are present in the patient –see (Adlassnig et al., 1986),(Adlassnig et al., 1985) or (Adlassnig, 1986) for more on the in- tended interpretation of v0–. However, other interpre- tations could also be suitable, at least to some extent. In fact, when defining the system CadPL in the next section, the interpretation to which we will commit will be probabilistic. The assignment v0 is defined for the negation of the entities in Γ and logical equivalents according to the following rule: If v0(θ) = η then v0(¬θ) = 1−η, for θ ∈ SL and η ∈ [0, 1].3 After the initial assignment the inference rules in ΦCB come into play. All the rules triggered by the sen- tences in Γ and its negations are used during the in- ference process. At each step in the inference process a rule is applied (that is done, in principle, in no partic- ular order). At the first step in the inference a rule of the form 〈θ,φ,η〉 in ΦCB is triggered, with η ∈ [0, 1] and θ,φ ∈ LLit. In order for that to happen θ or its negation needs to be in Γ and the value v0(θ) has to be strictly posi- tive if 〈θ,φ,η〉 is a rule in Φc and equal to 1 if the rule is in Φme or Φao. The application of the rule 〈θ,φ,η〉 generates a new assignment, v1, on {φ}. The value as- signed to φ by it is calculated as the minimum between η and v0(θ) and the value assigned to ¬φ and logical equivalents (if necessary for the inference) is calculated from v1(φ) as mentioned above for v0. At the nth step in the inference process a new rule of the form 〈θ,φ,η〉 in ΦCB will be triggered, for η ∈ [0, 1] and θ,φ ∈ LLit. At the nth step the application of this new rule will generate a new assignment on {φ} that will give φ the minimum between η and the value of θ considered for triggering the rule at this step in the inference. The value of θ needs to be strictly positive if the rule is of the type c and equal to 1 if it is of one 3 Notice that such a rule is compatible with a probabilistic interpretation of v0. 4 of the types me or ao. If the strictly positive values generated for θ before the nth step are multiple then the inference mechanism in CADIAG-2 will call the rule 〈θ,φ,η〉 again in further steps, if it has not done so previously, until all the values for θ have been used and all the possible values for φ generated. The assignment vn is defined for ¬φ as mentioned above for v0. The inference process goes on until all the rules trig- gered by all the sentences in Γ and its negations have been used and all the possible assignments for the sen- tences involved in the inference have been generated. CADIAG-2 yields as an outcome of the inference the set of medical entities in L occurring in the rules trig- gered by the initial evidence in Γ along with the max- imal value (with respect to the ordering � defined in Section 2) assigned to them during the inference. If a sentence is assigned both value 0 and 1 along the infer- ence process the system generates an error message. It is worth mentioning that the original inference process in CADIAG-2 works in a slightly different way. The update in the value of the distinct sentences in- volved in the inference is done as soon as two different values for the same sentence are produced by the sys- tem. The value chosen in the update for atomic sen- tences in L is the maximal one (with respect to the or- dering �). Notice though that this feature has a highly undesirable result (unless further restrictions on the rules or on the order in which the rules are applied are imposed), which is that the outcome of a run of the inference mechanism can depend on the order in which the rules are applied. Such a drawback is easily avoided by assuming that the update is only done at the end of the process. There are other several undesirable fea- tures about the inference in CADIAG-2, most of them related to the maximal value 0 and negated proposi- tions. Maybe the most evident concerning the maximal value 0 is that a medical entity that at some step along the inference process is assigned value 0 (that is to say, it is considered false with certainty or impossible) trig- gers any rules in which it occurs as the conditioning event if any other value other than 0 is assigned to it along the inference process. For a deeper analysis of such aspects of the inference process in CADIAG-2 see (Ciabattoni and Vetterlein, 2009). We represent sentences together with the assign- ments generated for them at each step in the inference by pairs in SL× [0, 1] along with a subscript indicating the step in the process at which such pairs have been generated. As mentioned above, a step in the inference process is given by the application of a rule in ΦCB and the new assignments that it generates for the sentences involved in the rule. Let p ∈ L and η ∈ [0, 1] be the highest assignment to p in a run of the inference mechanism in CADIAG-2. We will use the subscript max∗ on the pair (p,η) –that is to say, (p,η)max∗ – to denote that η is the maximal value assigned during the inference process for p (with respect to the ordering �). 4 THE FORMAL SYSTEM CADP L As seen in the previous section, the inference mech- anism in CADIAG-2 gets started by assigning to the ini- tial symptoms and diseases present in the patient (Γ) values in the interval [0, 1] (the initial assignment v0 to the entities in Γ and their corresponding negations). As mentioned earlier, such values stand in principle for fuzzy membership within the context of fuzzy set theory and are motivated by the vague nature of some medical entities that occur in CADIAG-2. In this paper though the interpretation that we will give to the assignment v0 will be probabilistic. Let us consider the medical entity ’reduced glucose in serum’. Let us assume that the value assigned by the evaluation system in CADIAG-2 (i.e., v0) to the state- ment ’Patient A has reduced glucose in serum’ out of the evidence given by the corresponding measurement of the amount of glucose in Patient A is η, for some η ∈ [0, 1]. As an example, we could interpret such value as the degree of belief that a medical doctor has in the truth of the statement given the evidence. As such η could be interpreted as a probability. The probabilistic interpretation is certainly favoured by the discretization applied to medical concepts in CADIAG-2 (for example, the concept ’glucose in serum’ generates five distinct medical entities in CADIAG-2: ’highly reduced glucose in serum’, ’reduced glucose in serum’, ’normal glucose in serum’, ’elevated glucose in serum’ and ’highly el- evated glucose in serum’). Notice that such an inter- pretation places us within the subjective probabilistic frame and thus, for the sake of coherence, the knowledge base ΦCB should also be interpreted subjectively. Other interpretations are also possible though. For example, one could regard such values as the ratio given by the number of doctors that agree on the truth of the state- ment out of all the doctors involved in the assessment. In order to accommodate such values into a coherent probabilistic frame along with the statements in ΦCB one could justify them as being subjective probabilities assessed by a group of experts –see (Genest and Zidek, 1986) or (Osherson and Vardi, 2006) for an analysis and justification of such concept–. Let p ∈ L represent a medical entity present in the patient and assume that η ∈ [0, 1] is the initial value 5 assigned to it by v0 at the start of a run of the infer- ence mechanism in CADIAG-2. We can formalise this by means of a probabilistic conditional statement rep- resented by a triple of the form 〈κ,p,η〉, where κ ∈ SL is the evidence that supports the presence of p in the patient. Next we will define the formal system CadPL. Re- call that the ultimate goal when doing so is to de- fine a system which represents the inference process in CADIAG-2 when interpreted from a probabilistic point of view. Although the inference in CADIAG-2 can be closely related to probability theory (given the nature of the rules of inference in ΦCB) it is not based on prob- abilistic methods and so the degree of freedom when choosing the rules of the system CadPL is high. We have chosen the rules by interpreting in the most nat- ural way the steps along the inference process within a probabilistic frame. The main idea behind such in- terpretation consists of the identification of the infer- ence process with the propagation of evidence facili- tated by the rules in ΦCB. For example, from 〈κ,φ,η〉, where κ ∈ SL is evidence supporting the presence of φ in the patient, and 〈φ,θ,ζ〉 in ΦCB we would infer 〈κ,θ, min(η,ζ)〉, where min(η,ζ) is the value (probabil- ity) assigned to θ given the evidence κ. We would have a propagation process of this nature for each single piece of evidence. The evidence would then be brought to- gether in CADIAG-2 by what we call the right conjunc- tion rule: given two outcomes of the inference process, say 〈κ1,p,η〉 and 〈κ2,p,ζ〉, for p ∈ L and κ1,κ2 ∈ SL, CADIAG-2 combines the evidence given by κ1 and κ2 by computing 〈κ1 ∧ κ2,p, max∗(η,ζ)〉. The inference rules of CadPL that we next present formalise this in- terpretation. A theory T in CadPL is a finite subset of K. A the- ory in our settings is not necessarily assumed to be con- sistent. In fact, ΦCB is not consistent as a probabilistic knowledge base, it contains a large number of conflicts (i.e., minimal inconsistent subsets) –see our compan- ion paper (Klinov et al., 2010) for more on the conflicts in ΦCB–. However, the inference engine in CADIAG-2 does not explode in the presence of such conflicts. For what follows let T = Ω ∪Φ1 ∪Φ2 be a theory, with Ω = {〈κ1,φ1,η1〉, ...,〈κm,φm,ηm〉}, for some m ∈ N, and Φ2 a set of triples of the form 〈θ,φ, 1〉, for θ,φ ∈ SL. Let CΩ = {κ1, ...,κm} and Γ = {φ1, ...,φm}. We will assume CΩ to be a consistent set (i.e., there exists a classical valuation that satisfies CΩ). Within the context of CADIAG-2, Γ is intended to represent the set of medical entities present in the pa- tient and Ω the initial assignment (v0) in the inference process given CΩ, the evidence in support of the pres- ence in the patient of the corresponding medical entities in Γ . The set Φ1 represents the rules of type c and Φ2 the rules of types me and ao. The formal system CadPL is defined by the follow- ing inference rules: – Reflexivity rule For φ ∈ SL, κ ∈CΩ and η ∈ [0, 1], 〈κ,φ,η〉 ∈ Ω T ` 〈κ,φ,η〉 – Negation rule For φ,ψ ∈ SL and η ∈ [0, 1], T ` 〈ψ,φ,η〉 T ` 〈ψ,¬φ, 1 −η〉 – Equivalence rule For ψ,φ,θ ∈ SL and η ∈ [0, 1], ψ ≡ φ T ` 〈θ,φ,η〉 T ` 〈θ,ψ,η〉 – Minimum rules For θ,φ ∈ SL, κ ∈CΩ, η ∈ (0, 1] and ζ ∈ [0, 1], First rule: T ` 〈κ,θ,η〉 〈θ,φ,ζ〉 ∈ Φ1 T ` 〈κ,φ, min(η,ζ)〉 Second rule: T ` 〈κ,θ, 1〉 〈θ,φ, 1〉 ∈ Φ2 T ` 〈κ,φ, 1〉 – Right conjunction rule For φ ∈ SL, C1,C2 ⊆CΩ and η,ζ ∈ [0, 1], T ` 〈 ∧ C1,φ,η〉 T ` 〈 ∧ C2,φ,ζ〉 T ` 〈 ∧ {C1 ∪C2},φ, max∗(η,ζ)〉 – Exhaustivity rule For φ ∈ SL, κ ∈CΩ, C ⊆CΩ and η ∈ [0, 1], T ` 〈 ∧ C,φ,η〉 ∀ζ ∈ [0, 1] T 0 〈κ,φ,ζ〉 T ` 〈κ∧ ∧ C,φ,η〉 Notice that the exhaustivity rule does not have any bearing on the decidability of whether 〈κ,φ,ζ〉 is prov- able from T or not for ζ ∈ [0, 1], φ ∈ SL and κ ∈ CΩ. The exhaustivity rule can only be applied after its prov- ability or non-provability has been decided. Given a theory T of CadPL and a triple Θ ∈ K, a proof of Θ from T is defined as a finite sequence of sequents of the form T ` Θ1, ...,T ` Θn 6 with Θn = Θ and where, for i ∈ {1, ...,n}, each Θi in T ` Θi follows from T by the application of one of the rules above, from Θj in a previous sequent (with j < i) or from Θj,Θk in previous sequents (with j,k < i) by one of the rules above. For what follows let Θ be the triple 〈θ,φ,η〉, for some η ∈ [0, 1] and θ,φ ∈ SL. Definition 6 We say that there exists a maximal proof of Θ from T if there exists a proof of Θ from T and there is no proof from T of 〈θ,φ,ζ〉 with η ≺ ζ. Definition 7 We say that Θ follows maximally from T (denoted by T `CadPL Θ) if there exists a maximal proof of Θ from T . For the next proposition let T = Ω ∪Φ1 ∪Φ2, with Ω = {〈κ1,q1,η1〉, ...,〈κm,qm,ηm〉}, Φ1 = Φ c and Φ2 = Φ me ∪ Φao, CΩ = {κ1, ...,κm} ⊂ SL and Γ = {q1, ...,qm} ⊂ L a set of medical entities occurring in ΦCB. Proposition 1 Let p ∈ L and η ∈ [0, 1]. We have that T `CadPL 〈 ∧ CΩ,p,η〉 if and only if (p,η)max∗ is the outcome of a run of the inference engine of CADIAG-2 on T . Proof 4 In order to prove the left implication let us consider a run of the inference engine of CADIAG-2 on T . The inference starts from pairs of the form (q,η)0 and (¬q, 1 − η)0 for some η ∈ [0, 1] for all q ∈ Γ . In CadPL a pair of the form (q,η)0, for q ∈ Γ , corresponds to a sequent of the form T ` 〈κ,q,η〉, for κ ∈ CΩ. The pair (¬q, 1 − η)0 corresponds to the sequent T ` 〈κ,¬q, 1−η〉. The former corresponds to an application of the reflexivity rule. The latter follows from the first one by an application of the negation rule. Let us assume now that we are at the nth step of the inference process and that a rule of the form 〈θ,φ,ζ〉 is triggered, for some ζ ∈ [0, 1] and θ,φ ∈ SL. Let us suppose that we have (θ,µ)n−t, the pair that triggers the rule at the nth step of the process, for µ ∈ (0, 1] and t ≤ n − 1. In CadPL that would cor- respond to a sequent of the form T ` 〈κ,θ,µ〉 de- rived from a previous step in the inference, for κ ∈CΩ. The inference mechanism in CADIAG-2 produces the pairs (φ, min(ζ,µ))n and (¬φ, 1−min(ζ,µ))n which, in the formal system CadPL, corresponds to the sequents 4 For the sake of brevity we will deal with sentences as if they were equivalence classes. If anything applies to a sentence of the form ¬φ, with φ ∈ SL, we also assume that it applies to any logical equivalent of ¬φ without mentioning it. T ` 〈κ,φ, min(ζ,µ)〉 and T ` 〈κ,¬φ, 1 − min(ζ,µ)〉 re- spectively, which follow by an application of one of the minimum rules and, for the latter, an application of the negation rule on the former. At the end of the process CADIAG-2 generates the pair (p,η)max∗ for each sentence p ∈ L involved in the inference, where η is the maximal value (with respect to the ordering �) among those assigned to p along the inference. This maximisation process is achieved in CadPL by means of repeated applications of the right conjunction rule. Instances of the exhaustivity rule (if necessary) complete the inferential counterpart of CADIAG-2 in CadPL. In order to prove the right implication let us suppose that we have a maximal proof of the form T ` Θ1, ...,T ` Θm, where Θm is the triple 〈 ∧ CΩ,p,η〉, for some η ∈ [0, 1] and p ∈ L. The first sequent of the proof needs to respond to an instance of the reflexivity rule, T ` 〈κ,q,η〉, for some q ∈ Γ, κ ∈ CΩ and η ∈ [0, 1]. The corresponding coun- terpart of this sequent in CADIAG-2 is the pair (q,η)0. Let us move now to the nth sequent, with n ≤ m. The nth sequent can be an instance of the reflexivity rule, T ` 〈κ,q,η〉, for some q ∈ Γ, η ∈ [0, 1] and κ ∈CΩ. The counterpart for this sequent in CADIAG-2 is the pair (q,η)0. The nth sequent can follow from a previous one in the proof by an instance of the negation rule. Let us suppose that the nth sequent is T ` 〈θ,¬φ, 1 − η〉 for some η ∈ [0, 1] and θ,φ ∈ SL and that there is a sequent T ` Θi, for some i < n, of the form T ` 〈θ,φ,η〉. The latter corresponds to a pair of the form (φ,η)t in CADIAG-2 and the former to the pair (¬φ, 1 − η)t, where t is the step in the inference process at which such pairs have been generated. The nth sequent can follow from a previous one by an instance of one of the minimum rules. Let us assume that the nth sequent is T ` 〈κ,φ, min(η,ζ)〉, for some φ ∈ SL, κ ∈ CΩ, η ∈ [0, 1] and ζ ∈ (0, 1], that T ` 〈κ,ψ,ζ〉 is a previous sequent in the proof and that 〈ψ,φ,η〉 is a rule in ΦCB. The latter corresponds in CADIAG-2 to the pair (ψ,ζ)t and the former to the pair (φ, min(η,ζ))t+k, where t,t + k indicate the steps at which the pairs have been generated by the inference process. The nth sequent can follow from previous sequents by an application of the right conjunction rule. The counterpart in CADIAG-2 of such an outcome consists of the maximisation process at the end of the inference. Instances of the exhaustivity rule are irrelevant to the inference in CADIAG-2. 7 This completes the proof. It is worth commenting on some features of the in- ference rules of CadPL in connection with probability theory. Soundness with respect to probabilistic seman- tics of the reflexivity, negation, and equivalence rules is clear. Soundness of the second minimum rule is also clear. The first minimum rule is certainly not sound with respect to such semantics. However, the right con- junction rule is not sound and the exhaustivity rule assumes some probabilistic independence among sen- tences that may not actually be independent. Overall, CadPL does not score well within probability theory. This is no surprise. The computation of conditional probabilistic statements in a compositional way, as done by CADIAG-2 primarily by means of the min and max∗ operators, is clearly bound to be probabilistically un- sound. One may wonder though what could be done in order to improve the inference on probabilistic grounds from a knowledge base like ΦCB. The answer seems to be ’not much’. Certainly a ΦCB-like knowledge base (i.e., a knowledge base given by some binary probabilis- tic conditional statements) is not the most convenient for inferential purposes in probability theory for medi- cal applications like CADIAG-2. As is well known, there are other knowledge-base structures better suited for that purpose, Bayesian networks being the most cele- brated among them, see (Castillo et al., 1997) or (Pearl, 1988). In terms of consistency, it is worth noting that CadPL satisfies what we can call weak consistency –called weak soundness in (Hajek, 1988)–, defined as follows: if there is a maximal proof in CadPL of a statement of the form 〈 ∧ ∆,φ, 1〉 (or 〈 ∧ ∆φ, 0〉) from a certain theory T , with φ ∈ SL and ∆ ⊆ SL then, if there is a maximal proof in CadPL of a statement of the form 〈 ∧ ∆∗,φ,η〉, with ∆ ⊂ ∆∗, then η = 1 (or η = 0 respectively). That is to say, if CadPL concludes certainty about the oc- currence of some event or about the truth or falsity of some sentence then adding new evidence does not alter this certainty. Weak consistency is provided in CadPL and so in the inference mechanism of CADIAG-2 by the operator max∗ defined over the ordering �. It is also worth noting that one could guarantee con- sistency (i.e., satisfiability) by relaxing the interpreta- tion of ΦCB and consider η in each triple 〈θ,φ,η〉 ∈ ΦCB a lower-bound probability threshold rather than a point-valued probabilitiy and by restricting the system to a positive fragment of LLit (i.e., only one of p, ¬p can occur in ΦCB). This way consistency is trivially guar- anteed for ΦCB together with any outcomes produced by the system during the inference process. In terms of soundness there does not seem to be much that one can do in order to improve the inference mechanism for knowledge bases like ΦCB, or at least not much that one can do that does not come at the price of generating probabilistic statements with very low prob- abilistic bounds (when working with lower-bound prob- ability thresholds), which would make CADIAG-2 po- tentially useless for practical purposes. There is some room for improvement for some steps in the inference that come by the addition of independence assump- tions among some of the medical entities in ΦCB. Under such independence assumptions a product rule instead of the minimum rule (i.e., composition through the product operator instead of the minimum one) could yield soundness in the context of lower-bound proba- bility thresholds for some inference steps. 5 CONCLUSION CADIAG-2 is a reasonably well-performing medical expert system (Adlassnig et al., 1986), but how it is so is far from clear. The inference engine of CADIAG-2 was built with methods of approximate reasoning in fuzzy set theory but, as such, it was not based on any logical formalism or theory embedded with a clear semantics. This fact motivated the main aim of this paper, which was no other than the understanding of CADIAG-2 in a logical way. The natural interpretation of the inference rules of CADIAG-2 (i.e., probabilistic) placed us upon the at- tempt of interpreting the inference itself probabilisti- cally. We formalised this interpretation by means of the system CadPL, the logical (probabilistic) counterpart of the inference engine of CADIAG-2. The unsoundness of some of the rules of CadPL (and thus of some infer- ence steps in CADIAG-2) and the inconsistency of the calculus (and thus of the inference process in CADIAG- 2) was made clear. Apart from these drawbacks, other- wise expected, some other aspects of CadPL were also stressed and analysed. At the end of the paper some possibilities for an improvement of CADIAG-2 in terms of soundness and consistency were also mentioned. Acknowledgements This research has been supported by the Vienna Science and Technology Fund (WWTF), Grant MA07− 016. I would like to thank A. Ciabattoni, T. Vetterlein and P. Rusnok for useful comments on previous drafts of this paper and for technical support with CADIAG-2. REFERENCES [Adlassnig, 1986]Adlassnig, K. (1986). Fuzzy set theory in medical diagnosis. IEEE Transactions on Systems, Man and Cybernetics, 16(2):260–265. 8 [Adlassnig et al., 1985]Adlassnig, K., Kolarz, G., Effen- berger, W., and Grabner, H. (1985). Cadiag: Ap- proaches to computer-assisted medical diagnosis. Computers in Biology and Medicine, 15:315–335. [Adlassnig et al., 1986]Adlassnig, K., Kolarz, G., Schei- thauer, W., and Grabner, H. (1986). Approach to a hospital-based application of a medical expert system. Informatics for Health and Social Care, 11(3):205–223. [Buchanan and Shortliffe, 1984]Buchanan, B. and Short- liffe, E. (1984). Rule-Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project. Addison-Wesley, Reading, MA. [Castillo et al., 1997]Castillo, E., Gutiérrez, J., and Hadi, A. (1997). Expert Systems and Probabilistic Net- work Models. Springer-Verlag, New York. [Ciabattoni and Vetterlein, 2009]Ciabattoni, A. and Vet- terlein, T. (2009). On the fuzzy (logical) content of cadiag2. Fuzzy Sets and Systems (to appear shortly). [Genest and Zidek, 1986]Genest, C. and Zidek, J. (1986). Combining probability distributions: A critique and an annotated bibliography. Statistical Science, 1(1):114–135. [Hajek, 1988]Hajek, P. (1988). Towards a probabilistic analysis of mycin-like expert systems. In COMP- STAT 88 proceedings. Physica-Verlag Heidelberg. [Hajek, 1989]Hajek, P. (1989). Towards a probabilistic analysis of mycin-like expert systems 2. In Artifi- cial Intelligence and Information-Control Systems of Robots. North-Holland. [Hajek, 1998]Hajek, P. (1998). Metamathematics of Fuzzy Logic. Kluwer, Dordrecht. [Hajek and Valdés, 1994]Hajek, P. and Valdés, J. (1994). An analysis of mycin-like expert systems. Math- ware and Soft Computing, 1:45–68. [Halpern, 2003]Halpern, J. (2003). Reasoning About Un- certainty. MIT Press. [Heckerman, 1986]Heckerman, D. (1986). Probabilistic in- terpretations for mycin’s certainty factors. In Un- certainty in Artificial Intelligence, pages 167–196. North-Holland. [Klinov et al., 2010]Klinov, P., Parsia, B., and Picado- Muino, D. (2010). The consistency of the cadiag- 2 knowledge base: A probabilistic approach. In LPAR. [Klir and Folger, 1988]Klir, G. and Folger, T. (1988). Fuzzy Sets, Uncertainty and Information. Prentice-Hall International. [Leitich et al., 2002]Leitich, H., Adlassnig, K., and Ko- larz, G. (2002). Evaluation of two different mod- els of semiautomatic knowledge acquisition for the medical consultant system cadiag2/rheuma. Arti- ficial Intelligence in Medicine, 25:215–225. [Osherson and Vardi, 2006]Osherson, D. and Vardi, M. (2006). Aggregating disparate estimates of chance. Games and Economic Behavior, 56:148–173. [Pearl, 1988]Pearl, J. (1988). Probabilistic Reasoning in Intelligent Systems. Morgan Kaufman, San Mateo, California. [Shortliffe, 1976]Shortliffe, E. (1976). Computer-Based Medical Consultations: MYCIN. Elsevier, New York. [Valdés, 1992]Valdés, J. (1992). An integrated environ- ment for uncertainty processing using graphical models. In IPMU 92 proceedings. [Zadeh, 1965]Zadeh, L. (1965). Fuzzy sets. Information and Control, 8:338–353. [Zadeh, 1975]Zadeh, L. (1975). Fuzzy logic and approxi- mate reasoning. Synthese, 30:407–428. [Zimmermann, 1991]Zimmermann, H. (1991). Fuzzy Set Theory and its Applications. Kluwer Academic Publisher, Boston - Dordrecht - London.