On combinations of local theory extensions

8 years 2 months ago
On combinations of local theory extensions
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 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 recogniz...
Viorica Sofronie-Stokkermans
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Viorica Sofronie-Stokkermans
Comments (0)