Benutzerhandbuch Datenschutzhinweis Impressum Kontakt





On Combinations of Local Theory Extensions


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

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.