@incollection{Sofronie-wlphg11,
TITLE = {On Combinations of Local Theory Extensions},
AUTHOR = {Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {0302-9743},
ISBN = {978-3-642-37650-4},
DOI = {10.1007/978-3-642-37651-1_16},
LOCALID = {Local-ID: 4D6F77024162244BC125784C00552BF9-Sofronie-wlphg11},
PUBLISHER = {Springer},
ADDRESS = {Berlin},
YEAR = {2013},
DATE = {2013},
ABSTRACT = {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.},
BOOKTITLE = {Programming Logics},
EDITOR = {Voronkov, Andrei and Weidenbach, Christoph},
PAGES = {392--413},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7797},
}