非表示:
キーワード:
-
要旨:
Many problems in mathematics and computer science can be
reduced to proving the satisfiability of conjunctions of
literals in a background theory which is often the extension
of a base theory with additional functions or a combination
of theories.
It is therefore important to have efficient procedures for
checking satisfiability of conjunctions of ground literals
in extensions and combinations of theories.
For a special type of theory extensions, namely \em local
extensions, hierarchic reasoning, in which a theorem prover
for the base theory can be used as a ``black box'',
is possible. Many theories used in computer science or
mathematics are local extensions of a base theory.
However, often it is necessary to consider complex extensions
of a theory, with various types of functions.
In this paper we identify situations in which
a combination of local extensions of a base theory
is guaranteed to be again a local extension of the base theory.
We thus obtain criteria both for recognizing wider classes of
local theory extensions, and for modular reasoning in
combinations of theories over non-disjoint signatures.
