A topic of research at CLC - FibLog project.
Besides leading to very interesting applications whenever it is necessary to work with different
logics at the same time, combination of logics is also of interest on purely theoretical grounds.
The practical significance of the problem is clear, at least from the point of view of those working in knowledge
representation (within artificial intelligence) and in formal specification and verification (within
software engineering). Indeed, in these fields, the need for working with several
formalisms 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 both temporal and deontic
aspects. And in a software specification problem it may be necessary to work with both equational and temporal
specifications.
From a theoretical point of view, one might be tempted, for instance, to look at predicate temporal logic as resulting from
the combination of first order logic and propositional temporal logic. But the approach will be significant if and only if
general preservation results are available about the mechanism used for combining the logics. For example, if it has been
established that completeness is preserved by the combination mechanism
@ and it is known that logic L is given by L'@L'', then the completeness of the combination
L follows from the completeness of L' and L''. No wonder that much theoretical effort
has been dedicated to establishing preservation results and/or finding preservation counterexamples.
Among the different techniques for combining logics, fibring, as originally proposed by Dov Gabbay, deserves close study because of its generality and power. Fibring explains many other combination mechanisms as special cases and it is powerful enough for the envisaged applications.
But what is fibring? The answer can be given in a few paragraphs for the special case of logics with a
propositional base, that is, with propositional variables and connectives of arbitrary arity.
The language of the fibring is obtained by the free use of the language constructors (atomic symbols and connectives) from the
given logics. So, for example, when fibring a temporal logic and a deontic logic,
mixed formulae such as
((G a) -> (O(Fb)))
appear in the resulting logic. Naturally, in many cases we want to share some of the symbols. The previous
example involves the constrained form of fibring imposed by sharing the common propositional part.
At the deductive system level, provided that the two given logics are endowed with deductive systems of the same type, the
deductive system of the fibring will be obtained by the free use of the inference rules from both. This approach will be of
interest only if the two given deductive systems are schematic in the sense that their inference rules are
open
for application to formulae with foreign symbols (from the other logic). For instance, when
we define MP by the inference rule
{(x -> y), x} |- y
in some Hilbert system, we may implicitly assume that the instantiation of the
metavariables x, y by any formulae, possibly
with symbols from both logics, is allowed when applying MP in the fibring.
The semantics of fibring is more complicated and, therefore, it is better to consider the special case where both logics have
semantics with similar models. A possible, quite general, model for many logics with a propositional base is provided by a
triple
< U, B, v >
where U is a set (of points, worlds, states, whatever), B is a subset of the parts of U, and v(c) is a map from B^n to B for each language constructor c of arity n. In what follows we consider only logics with a semantics given by a class of such triples.
Given two such logics L', L'' what should be the semantics of their fibring? It will be a class of models of the form above, such that, at each point u of U, it is possible to extract a model from L' and one from L''. If symbols are shared, the two extracted models should of course agree on them.
In order to visualize the semantics of fibring, consider the fibring of a propositional linear temporal logic with a propositional linear space logic. Each model of the fibring will be a cloud of points where at each point we know the time line and the space line crossing there. For instance, at the point
< Lisbon, 10h15m 28 January 2002>
we know the time line (of past, present and future) of Lisbon and the space line (the universe taken as a line for the sake of the example) at 10h15m 28 January 2002.
D. Gabbay. Fibred semantics and the weaving of logics: part 1. Journal of Symbolic Logic, 61(4):1057-1120, 1996.
D. Gabbay. Fibring logics. Oxford University Press, 1999.A. Sernadas and C. Sernadas. Combining logic systems: Why, how, what for? CIM Bulletin, 15:9-14, 2003.
A. Sernadas, C. Sernadas, and C. Caleiro. Fibring of logics as a categorial construction. Journal of Logic and Computation, 9(2):149-179, 1999.
A. Zanardo, A. Sernadas, and C. Sernadas. Fibring: Completeness preservation. Journal of Symbolic Logic, 66(1):414-439, 2001.
Last update: February 16, 2004.