A General Framework for Multi-Theory Logic Languages

Multi-theory logic languages are a wide class of programming languages which extend the standard logic programming paradigm by partitioning the logic program into a multiplicity of logic theories. Such an extension is generally meant to address typical software engineering issues, such as modularity, component reuse, incremental software design and development. Despite of the many syntactic and semantic differences, what multi-theory logic languages share is the partitioning of the program according to the abstractions of the domain of discourse, by associating different collections of axioms to different domain elements. The aim of this work is then to introduce a general framework for multi-theory logic languages, providing a uniform approach for their definition and description. An extended notion of logic formula is introduced, which makes the relationship between formulae and domain abstractions explicit. A class of extended logic languages is consequently defined, which is general enough that any multi-theory logic language can be mapped onto it through suitable translation functions. Such languages, called scope languages, can then be used as a mean to express the semantics of any multi-theory logic language, and as a tool for the comparison of different languages of that kind.