Automated Reasoning in Extensions and Combinations of Logical

decidable and tractable fragments of (first- or higher-order) logic, and
to develop efficient deductive calculi for these fragments. However, in
most real-life applications it is necessary to consider combinations of
theories which are, usually, extensions of a shared base theory. Two
important questions arise in this context:

(1) Assume that we have a complete prover for a logical theory. Can one
use this prover as a "black box” to prove theorems in an extension of
the theory?

(2) Assume that we have complete provers for two theories. Can we obtain
a complete prover for their combination, by using the provers of the
components as “black boxes”?

In this lecture several situations in which hierarchical and modular
reasoning is possible are presented and similarities and differences
between various approaches to modular theorem proving in combinations of
logical theories are pointed out.