English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Hierarchic reasoning in local theory extensions

MPS-Authors
/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Sofronie-Stokkermans, V. (2005). Hierarchic reasoning in local theory extensions. In R. Nieuwenhuis (Ed.), Automated deduction - CADE-20: 20th International Conference on Automated Deduction (pp. 219-234). Berlin, Germany: Springer.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2898-5
Abstract
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.