There have been several attempts to formalize the various conceptual models of medical diagnosis. The most important, but not all, formal theories of medical diagnosis are reviewed below:

ConsistencyBased Diagnosis: The formal theory of diagnosis originally proposed by Reiter was motivated by the desire to provide a formal underpinning of diagnostic problem solving using knowledge of the normal structure and behavior of technical devices, i.e. DNSB diagnosis. Reiter’s theory of diagnosis is often referred to as the ConsistencyBased Theory of Diagnosis, or ConsistencyBased Diagnosis for short. According to the Reiter’s definition, a diagnosis in the theory of consistency based diagnosis can be defined as follows: Let be a system, where denotes a finite set of formulae in firstorder predicate logic, specifying normal structure and behavior, called the system description; denotes a finite set of constants (nullary function symbols) in firstorder logic, denoting the components of the system; and denotes a finite set of formulae in firstorder predicate logic, denoting observations, i.e. observed findings. Now let be the set of all positive ‘Abnormal’ literals, and be the set of all negative ‘Abnormal’ literals. Furthermore, let be a set, called a hypothesis, such that: for some . Then, the hypothesis is a consistencybased diagnosis of if the following condition, called the consistency condition, holds true: , i.e. is consistent. The consistency condition captures DNSB diagnosis in terms of consistencybased diagnosis under the assumption that the axioms in provide a completely accurate representation of a physical system. A diagnosis is just a hypothesis that is accepted.

Abductive Diagnosis: The formalization of MAB diagnosis has been extensively studied by Console and Torasso. In their theory, the abnormal behavior of a system is specified in terms of abnormal states and resulting abnormal findings. Normal findings may also be included, but these are less useful for diagnosis, since an abnormal state is often causally related to a large number of normal findings. Diagnostic problem solving is formally described as the problem of accounting for a given set of observed findings, referred to in the theory as manifestations, by the simulation of abnormal behavior. The simulation process is accomplished by deduction with logical axioms, describing abnormal behavior, and assumed (abnormal) states. According to the theory of diagnosis by Console and Torasso, stands for a causal specification, where denotes a set of possible defect and assumption literals; denotes a set of possible (positive and negative) observable finding literals; and (Causal Model) stands for a set of logical (abnormality) axioms. Then, a hypothesis is called a prediction for a set of observable findings if:
(۱) , and
(۲) is consistent.
Now an abductive diagnostic problem is defined as a pair , where is called a set of observed findings. Formally, a solution to an abductive diagnostic problem can be defined as a hypothesis if:
(۱) (covering condition);
(۲) (consistency condition)
where is defined by: . In fact, the set stands for findings assumed to be false, because they have not been observed (and are therefore assumed to be absent). But any finding may also be unknown. Thus, rather than providing a single definition, Console and Torasso provide several alternatives in their articles for this set , and the definition provided above is just one of the alternatives. In this case, an entire solution may be taken as a diagnosis, but a diagnosis is formally considered to consist of the defect literals in a solution . So if be a solution to an abductive diagnostic problem , then, the set of all defects is called an abductive diagnosis of . 
SetCovering Theory of Diagnosis: Instead of choosing logic as the language for MAB diagnosis, as discussed above, others have adopted set theory as their formal language. This approach to the formalization of diagnosis is referred to as the SetCovering Theory of Diagnosis, or Parsimonious Covering Theory. The treatment of the setcovering theory of diagnosis in the literature deals only with the modeling of restricted forms of abnormal behavior of a system. In the setcovering theory of diagnosis, the triple is formally called a causal net; where is a set of possible defects; is a set of elements called observable findings; and is a binary relation, , called the causation relation. A diagnostic problem in the setcovering theory of diagnosis is then defined as a pair , where is a set of observed findings. It is assumed that all defects are potentially present in a diagnostic problem, and all findings will be observed when present. In addition, all defects have a causally related observable findings , and vice versa, i.e. , and . No explicit distinction is made in the theory between positive (present), negative (absent) and unknown defects, and positive (present), negative (absent) and unknown findings. The causation relation is often depicted by means of a labeled, directed acyclic graph, which, as , is called a causal net. Now let denote the power set of the set . It is convenient to write the binary causation relation as two functions. The first function,
called the effects function, is defined as follows; for each :
, where and the second function,
called the causes function, is defined as follows; for each :
, where .
A causal net can now be redefined, in terms of the effects function above, as a triple . Given a set of observed findings, diagnostic problem solving amounts to determining sets of defects —technically the term cover is employed— that account for all observed findings. Formally, a diagnosis is defined as follows: Let be a diagnostic problem, where is a causal net, and denotes a set of observed findings. Then, a setcovering diagnosis of is a set of defects , such that:
A set of defects is said to be an explanation of a diagnostic problem , with a set of observed findings, if is a diagnosis of and satisfies some additional criteria. Various criteria, in particular socalled criteria of parsimony, are in use. The basic idea is that among the various diagnoses of a set of observable findings, those that satisfy certain criteria of parsimony are more likely than others. If be a diagnostic problem, then some of the criteria as mentioned in different papers are: minimal cardinality, irredundancy, relevance and most probable diagnosis. In addition, another condition called minimalcost diagnosis is defined. According to this condition, a diagnosis of a set of observed findings is called a minimalcost explanation of if and only if:
for each diagnosis of , where cost is a function associating real values with defects . The cost of a diagnosis may be anything, varying from financial costs to some subjective feeling of importance expressed by numbers. However, many choose as semantics of cost function information for the negative logarithm of probabilities. Under this interpretation, a minimalcost diagnosis is identical to a most probable diagnosis. Although not every diagnosis is an explanation, any diagnosis may be seen as a solution to a diagnostic problem, where diagnoses which represent explanations conform to more strict conditions than others. 
Hypothetico Deductive Diagnosis: The third approach to diagnosis, AC diagnosis, originates from work by E. H. Shortliffe and his colleagues in the MYCIN project. The knowledge incorporated in that expert system, and in similar systems for AC diagnosis, is based on the body of experience accumulated ill handling a large number of cases, such as the patients a physician sees in medical practice. It has usually called this type of knowledge empirical associations, i.e. the knowledge consists of associations between typical observable findings and defects; and knowledge about the underlying mechanisms (if available) is not represented. Hence, we shall refer to this formal counterpart of AC diagnosis as HypotheticoDeductive Diagnosis. Now let denote an associational specification, where denotes a set of (positive and negative) possible defects, denotes a set of (positive and negative) observable findings, and denotes the logical representation of a set of empirical associations. A hypotheticaldeductive diagnostic problem is then defined as a pair , where denotes a set of observed findings. Thus, a diagnosis based on empirical associations can be defined as follow: Let be a set of defects, called a hypothesis. Then, is called a hypotheticodeductive diagnosis of if and only if . Note that, in contrast with the theories discussed above, a single hypothesis is initially given in hypotheticodeductive diagnosis and it stands for the defects that are initially given to be of interest.