非表示:
キーワード:
-
要旨:
We show that for special types of extensions of a base theory,
which we call {\em local},
efficient hierarchic reasoning is possible.
We identify situations in which it is possible,
for an extension ${\cal T}_1$ of a theory ${\cal T}_0$,
to express the decidability and complexity of the
universal theory of ${\cal T}_1$ in terms of
the decidability resp.\ complexity of suitable
fragments of the theory ${\cal T}_0$ (universal or $\forall \exists$).
These results apply to theories related to data types,
but also to certain theories of functions from mathematics.
