An initiative of SQIG at IT partially supported by FCT and EU FEDER, namely via projects KLog PTDC/MAT/68723/2006, QSec PTDC/EIA/67661/2006 and AMDSC UTAustin/MAT/0057/2008.
Since the pioneering works by Thomason 1984 and Konolidge 1986, the problem of combining logics (and proving transference results about the combination mechanisms) has attracted growing attention. The practical motivation is clear: in applications (e.g. software engineering and artificial intelligence), the need to work with several logics at the same time is the rule rather than the exception. Ideally, the practitioner instead of developing from zero a new logic with the envisaged features would combine well known logics and use the transference results on the adopted combination mechanism to infer the properties (e.g. completeness) of the resulting logic from those of the combined logics. A plethora of combination mechanisms has been proposed, namely fusion (Kracht and Wolter 1991), temporalization (Finger and Gabbay 1992), combination of institutions (Tarlecki 1995) and fibring (Gabbay 1996), synchronization (Sernadas et al 1997), product (Gabbay and Shehtman 1998) and modalization (Fajardo and Finger 2003). A few transference results have been established, namely: preservation of weak completeness and decidability by modalization; weak completeness, finite model property and Craig interpolation by fusion; weak and strong completeness, Craig interpolation and finite model property by fibring. An effort has been made to enlarge the domain of applicability of the combination mechanisms to a wider class of logics: for instance, fibring subsumes fusion and it is applicable well beyond the realm of modal logics. In this vein, the graph-theoretic account of fibring recently proposed by Sernadas et al 2009 further extends its domain of applicability to substructural logics, including linear and paraconsistent logics. Some work has been dedicated to applying the categorical imperative to this field, namely setting up an appropriate category of logics where fibring appears as a universal construction, as initially advocated by Sernadas et al 1999. However, the required morphisms are rather awkward. Recently, we proposed to recover Winskel's idea (1984) of using partial morphisms for the parallel composition of processes. This idea when applied to logics led us to yet another mechanism for combining logics (parallel composition) that turned out to subsume fibring as a special case and stressed the importance of combining connectives (and other language constructors). Basing the combination of logics on such combinations of constructors opened the way towards a more conservative combination mechanism (meet-combination), by endowing each combined constructor only with the common logical properties of its components.
The initiative aims at further exploration of the graph-theoretic account of logics and their combinations, addressing logics with quantification, establishing further transference results about combined logics and their theories, relating different combination mechanisms, and taking advantage of the suitability of the graph-theoretic semantics for applications in model checking and security.
AMS-MSC 03B62 Combined logics