Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Hierarchic Reasoning in Local Theory Extensions
verfasst von : Viorica Sofronie-Stokkermans
Erschienen in: Automated Deduction – CADE-20
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We show that for special types of extensions of a base theory, which we call
local
, efficient hierarchic reasoning is possible. We identify situations in which it is possible, for an extension
$\mathcal{T}_{1}$
of a theory
$\mathcal{T}_{0}$
, to express the decidability and complexity of the universal theory of
$\mathcal{T}_{1}$
in terms of the decidability resp. complexity of suitable fragments of the theory
$\mathcal{T}_{0}$
(universal or ∀ ∃). These results apply to theories related to data types, but also to certain theories of functions from mathematics.