de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Impressum Kontakt Einloggen

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Buchkapitel

#### On Combinations of Local Theory Extensions

##### MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45516

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

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

Sofronie-Stokkermans, V. (2013). On Combinations of Local Theory Extensions. In A. Voronkov, & C. Weidenbach (Eds.), Programming Logics (pp. 392-413). Berlin: Springer. doi:10.1007/978-3-642-37651-1_16.

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.