3.3 Theorem Provers and Other Reasoners 57
logical theories that corresponds to type checking in modern programming
languages. If one uses a theorem prover for consistency checking, the result
will normally be only one of these three possibilities: consistent, inconsistent,
or unknown. By contrast, with a rule engine the result will also show, in
some detail, the reasons why the theory is inconsistent or why the theory
could not be shown to be either consistent or inconsistent. Needless to say,
this is much more useful. Of course, some theorem provers are much better
at explaining the reason for their conclusion, but the most popular ones give
up this capability for the sake of efficiency.
Theorem provers use a variety of strategies, and many systems offer sev-
eral strategies and considerable customization of those strategies. Theorem
proving in general is undecidable, so there is always a possibility that an
attempt to prove a theorem will fail. One popular strategy is the use of
“tableaux.” When attempting to prove a theorem, one must try many pos-
sibilities. When one attempt fails, it is necessary to backtrack to an earlier
point in the attempt and then try again. From this point of view, theorem
proving is a search in a very large (potentially infinite) space of proofs, and
tableaux are a means of controlling the search.
Because theorem provers and rule engines can be inefficient, a large num-
ber of specialized automated reasoners have been introduced that are limited
to specific kinds of reasoning problems but are much more efficient than the
general reasoners. We discuss some of the most popular of these in this sec-
tion.
Constraint solversallow one to specify a collection of constraints on vari-
ables. The constraints are most commonly linear equalities or inequalities,
and the variables are usually real-valued. A solution is an assignment of real
values to the variables so that all of the constraints hold. Sometimes one also
asks for the solution that maximizes some linear function. Constraint solvers
are not reasoning about the variables in the same way that rule engines and
theorem provers are reasoning about their variables. However, constraint
solvers are sometimes sufficient for some classes of reasoning problems, and
they are much more efficient at finding solutions than a rule engine or theo-
rem prover would be on the same problem.
Although constraint solvers are excellent for multivariate constraint prob-
lems, they are rarely compatible with the reasoning needed for ontologies.
So they will not be discussed in any more detail.
Description logic(DL) reasoners are a form of theorem prover that is opti-
mized for a special class of theories. Biological information captured using
DLs is classified in a rich hierarchical lattice of concepts and their interrela-