Tableaux Handbook
Bernhard Beckert
Equality and Other Theories
Theory reasoning is an important technique for increasing the efficiency
of automated deduction systems. The knowledge from a given domain (or
theory) is made use of by applying efficient methods for reasoning in
that domain. The general purpose foreground reasoner calls a special
purpose background reasoner to handle problems from a certain theory.
Theory reasoning is indispensable for automated deduction in real world
domains. Efficient equality reasoning is essential, but most
specifications of real world problems use other theories as well:
algebraic theories in mathematical problems and specifications of
abstract data types in software verification to name a few.
Following the pioneering work of M. Stickel, theory reasoning methods
have been described for various calculi; e.g., resolution, path
resolution, the connection method, model elimination, connection
tableaux, and the matrix.
In this chapter, we describe how to combine background reasoners
with the ground, the free variable, and the universal formula versions
of semantic tableaux. All results and methods can be adapted to
other tableau versions for first-order logic: calculi with signed
formulae, with different $\delta$-rules, with methods for restricting
the search space such as connectedness or ordering restrictions, with lemma
generation, etc. Difficulties can arise with adaptations
to tableau calculi for other logics, in particular if the consequence
relation is affected (e.g., non-monotonic logics and linear logic); and
care has to be taken if theory links or theory connections have to be
considered.
One main focus of this chapter is efficient equality reasoning in
semantic tableaux. Equality, however, is the only theory that is
discussed in detail. There is no uniform way for handling theories,
which is, after all, the reason for using a background reasoner but
which makes it impossible to present good background reasoners for all
possible theories. The second main focus of this chapter is therefore on
the interaction between foreground and background reasoners, which plays
a critical role for the efficiency of the combined system.