Combining logic systems: Why, how, what for?
Amı́lcar Sernadas, Cristina Sernadas · 2003
The practical significance of the problem of combining logics is widely recognized, namely in knowledge representation (within artificial intelligence) and in formal specification and verification of algorithms and protocols (within software engineering and security). In these fields, the need for working with several calculi at the same time is the rule rather than the exception. For instance, in a knowledge representation problem it may be necessary to work with temporal, spatial, deontic and probabilistic aspects (e.g., for reasoning with mixed assertions like “with probability greater than 0.99, sometime in the future smoking will be forbidden everywhere”). And in a software verification problem it may be necessary to mix equational, epistemic and dynamic logic features. That is, one needs, at least, to be able to develop theories with components in different logic systems, or, even better, to work with theories defined in the combination of those logic systems (where such mixed assertions are allowed). Motivated by these applications that require the joint use of several deduction formalisms, the interest in combination of logic systems has recently been growing