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...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Viorica Sofronie-Stokkermans
• Keywords: Base Theory, CORR 2008, Education, Local Extension, Theory