On combinations of local theory extensions

TL;DR

This paper explores efficient reasoning methods in combined theories with possibly overlapping signatures, introducing local extensions and criteria for their modular combination to enhance hierarchical reasoning in computer science and mathematics.

Contribution

It introduces the concept of local theory extensions and provides criteria for their modular combination, enabling hierarchical reasoning in complex theory systems.

Findings

Identification of local theory extensions enabling hierarchical reasoning

Criteria for combining local extensions over non-disjoint signatures

Examples from computer science and mathematics illustrating natural occurrences

Abstract

In this paper we study possibilities of efficient reasoning in combinations of theories over possibly non-disjoint signatures. We first present a class of theory extensions (called local extensions) in which hierarchical reasoning is possible, and give several examples from computer science and mathematics in which such extensions occur in a natural way. We then identify situations in which combinations of local extensions of a theory are again local extensions of that 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.