Multi-context Logics—A General Introduction

Abstract

Multi-context logics (MCLs) constitute a family of formalisms that allow one to integrate multiple logical theories (contexts) into an articulated structure, where different theories can affect one another via so-called bridge-rules. In the past 20 years multi-context logics has been developed, for contexts in propositional logics, first order logics, description logics and temporal logic. Each of these logics has been developed, in an independent manner, for representing and reasoning about contextual knowledge in a specific application domain instead of originating from a single general formal framework. The absence of such a general formal framework for Multi-Context Systems (MCS), from which to extract tailored versions for the different application domain, has led to the development of a rather heterogeneous family of formal systems, whose comparison is sometimes very difficult. Being able to represent all these systems as specifications of a general class would be very useful as, for instance, one could reuse results proven in one MCS in another one. In this chapter, the authors provide an a-posteriori, systematic, and homogeneous description of the various MCSs introduced in the past. The authors do this firstly by providing a general definition of the MCS framework with its main components, which is general enough to capture the various versions of MCSs. Then, an account of the main logical specialisations of the MCS framework is provided, with an explanation of the domain of application they have been developed for.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Multi-context logics (MCLs) are a family of formalisms for the integration of multiple logical theories (contexts) in an articulated composite structure. They are based upon two key principles of contextual knowledge, named principle oflocality and principle ofcompatibility (Ghidini and Giunchiglia2001). The principle of locality states that a context represents (or, in a more technical fashion, axiomatizes in a logical theory) a portion of the world, and that every statement entailed by such a representation is intended to hold within that portion of the world. The principle of compatibility instead states that different contexts that describe overlapping portions of world are represented by compatible logical theories, which are constrained to describe compatible situations. To illustrate these principles, and the idea of context underlined by MCLs we recall here the magic box example originally introduced in Ghidini and Giunchiglia (2001).

Fig. 25.1

The magic box.a The complete scenario.b Mr. 1 andMr. 2’s views.c Incompatible views

Example 1

Consider the scenario of Fig. 25.1a. Two observers,Mr. 1 andMr. 2, are looking at a rectangular glass box from two different perspectives, one from the front, and one from the side. The box consists of six sectors, each sector possibly containing a ball. The box is “magic” and observers cannot distinguish the depth inside it. Figure 25.1b shows whatMr. 1 andMr. 2 can see in the scenario depicted in Fig. 25.1a.

In this example we have two contexts, each context describing what an observer sees (its viewpoint) and the consequences that it is able to draw from it. The content of the two contexts is graphically represented in Fig. 25.1b. Notice that here the term context does not refer to a particular circumstance, or state of affair, but it refers to the point of view of each agent. Indeed we use the expression “the context of agent 1 (or 2)” to indicate his/her point of view.

Concerninglocality, bothMr. 1 andMr. 2 have the notions of a ball being on the right or on the left. However there may be situations in which there is a ball which is on the right forMr. 1 and not on the right forMr. 2. FurthermoreMr. 2 has the notion of “a ball being in the center of the box” which is meaningless forMr. 1.

Concerningcompatibility, the partial representations ofMr. 1 andMr. 2’s contexts are obviously related. The relation is a consequence of the fact thatMr. 1 andMr. 2 see the same box. Figure 25.1b shows a pair of two compatible representations (contexts), while Fig. 25.1c shows a pair of incompatible representations (contexts). In this simple example we can synthetically describe all the compatible representations using a narrative like: “ifMr. 1 sees at least a ball thenMr. 2 sees at least a ball”.

The MCL representing the magic box scenario is composed of:

• Two logical theoriesT ₁ andT ₂, each of them containing the logical representation of the context that describes one of the observer’s viewpoints over the box. Each logical theoryT _i will be described using an appropriate, and possibly different, logicL _i , interpreted in its own set of local models.

• A description of how to constrain the individual logical theories (and similarly the underlying logical models) in pairs that represent compatible viewpoints.

By generalising from the above example, the basic framework of MCLs is constituted by a number of logical theoriesT _i , each of them used to represent a context by means of an appropriate logicL _i , plus a description of how to combine/constrain the individual logical theories in compatible sequences that represent the entire multi-context structure. In the past 20 years this basic framework of MCL has been developed to model contexts described by means of different types of logic. In this chapter we provide an account of the main logical specialisation of MCLs, namely propositional logic and first order logic Multi-context Logics with an explanation of the types of applications they have been used for.

The chapter is structured as follows. In Sect. 25.2 we introduce the general definition of Multi Context Logic with its basic components, namely: syntax, semantics, logical consequence and deductive system (in literature called Multi Context System). MCLs can be categorized in two main families, namely: propositional MCL and quantificational MCL. In Sect. 25.3 we introduce the general definition of propositional MCL and some of the MCL that have been proposed in the past. In Sect. 25.4 we introduce quantificational MCLs and its two main important instances: Distributed First Order Logics and Distributed Description Logics.

2 Multi-context Logics

It its more general form, amulti-context logic (MCL) is defined on a family of logics$\{L_i\}_{i\in I}$ where eachL _i is a logic used to formalize thei-th context. We assume that each logicL _i is equipped with a formal language, a class of structures in which this language is interpreted, a satisfiability relation (denoted by ⊧ _i ) which defines when a formula is true or false in an interpretation structure, and a logical consequence relation (also denoted by ⊧ _i ), that states when a formula is a logical consequence of a set of formulas of the language ofL _i .

2.1 Languages of MCL

We distinguish two main categories of MCL: propositional and quantificational MCL, depending on the fact the languages associated to each context, are only propositional or quantificationals. By propositional languages we refer to logical languages that contain only expressions that express that a certain state of affair has a certain truth value (independently from the specific truth value). Quantificational languages extend propositional languages with the possibility of specifying objects of the domain, by means of special expressions usually called terms. In the case of quantificational multi-context logic we extend the language ofL _i (with$i\in I$) with a set of terms calledarrow variables, denoted as$x^{\rightarrow j}$ and$x^{j\rightarrow}$, (withx variable and$j\in I$). Arrow variables are used to point to objects to other domains. The formal semantic will be clarified later.

2.2 Multi-context Structure

The setI of context indexes (aka context names) can be either a simple set, or a set equipped with an algebraic structure such as, for instance a partial order, a lattice, a linear order, and possibly a set of operations on context indices. For instance, a partial order structure$\left<I,\prec\right>$ can be used to represent a set of contexts which are organized according to a general-specific relation. For instance iffootball is the context (theory) that formalizes the domain of football, whileSport is the context (theory) that formalizes the more general domain of sport, the fact that the football domain is more specific than the sport domain can be captured by imposingfootball≺sport inI. A discrete linear order can be used to represent the evolution of the knowledge of one or a group of agents, where each context formalizes the agents’ knowledge state at a given stage. For instance ificd10 is the context that describes the international classification diseases - version 10, andicd11 is the context that describes the the next version of the same classification, then$\textsc{icd10}\prec\textsc{icd11}$ states thaticd11 is the subsequent version oficd10. Finally a lattice structure can be adopted to represent knowledge which holds in convex time intervals (represented by pairs of time points$\left<start,end\right>$. The containment relation between intervals, represents the fact that the temporal span of a context covers the temporal span of another context.

2.3 Multi-context Model

Amodel for a multi-context logic$\{L_i\}_{i\in I}$ is a class of functionsC where each function$c\in C$ assigns to each element$i\in I$ a set of interpretationsc _i for the logicL _i . Each element ofc _i is called alocal model ofL _i , and every$c\in C$ is called achain ¹. Figure 25.2 provides a graphical illustration of a chain for a set of four contexts.

Fig. 25.2

A multi-context model. Each language is interpreted in a set of models. Each combination of sets of local models defines a chain and belongs to a compatibility relation. Graphically (and formally) this can be thought as an iper-arc on the graph of a set of sets of local models

A multi-context model is also calledcompatibility relation to emphasize the fact that it describes a class of compatible combinations of local models that mimic the type of relation that is assumed to hold between the original contexts they represent.

Some additional definitions are necessary to define the semantics for quantificational MCL. Quantificational logics extend propositional logics with the capability of predicating properties of objects of a universe, by introducing a class of expressions that denote objects of a domain. These expressions are usually called terms. As happens for propositional formulas, terms in different contexts can have different meaning. Classical examples of terms with context dependent meaning taken from the area of formal linguistics are indexicals (like “here”, “now”, “me”); other examples can be found in the area of heterogeneous information integration, where a term can be used differently in different information resources (e.g., “Trento” in a database can be used to denote the province of Trento, while in another one is used to denote the city of Trento). Conversely, meaning of terms in different contexts can be related. To capture the relations between elements of different domains of interpretation we introduce the notion ofdomain relation. More precisely, let Δ^m be the domain of a local modelm, and$\Delta_i=\bigcup_{m\in c_i}\Delta^m$,$\Delta_j=\bigcup_{m\in c_j}\Delta^m$ be the domains of interpretation for the models inc _i andc _j respectively, {then adomain relation r _ij fromi toj is any subset of$\Delta_i\times\Delta_j$}.²

For instance suppose thatA is the context corresponding to the database of books available on a web catalogue (say Amazon), andB is the database of the physical copies of books available in a library (say Biblioteca di Trento). A chain for the MCL composed ofA andB is a pair$\left<c_A,c_B\right>$. To represent the correspondence between the books titles available on Amazon and the book copies available in the Library of Trento, we can use ther _AB , that contains each pairs$\left<a,b_1\right>,\dots,\left<a,b_k\right>$ where$b_1,\dots,b_k$ are the$k\geq 1$ copies of the booka sold by Amazon, which are available in the library of Trento.

2.4 Multi-context Satisfiability

Satisfiability is a relation that spans between a model and formulas belonging to different logical languages, which are not necessarily disjoint. This introduces the necessity to distinguish between formulas that occur in different contexts. Alabelled formula is an expression of the form$i:\phi$ where φ is a well formed formula ofL _i . The intuitive meaning of$i:\phi$ is that φ holds in thei-th context.

Local satisfiability, that is, the satisfiability of a formula φ in a contexti, is defined w.r.t. the local models and, possibly, the assignments to the free variables occurring in φ in case of quantificational contexts. Intuitively, a labelled formula$i:\phi$ is satisfied by a modelC {if all the local models$m\in c_i$ for all the chains$c \in C$ satisfy φ.}

Fig. 25.3

A MCL model

To make a simple example, consider the MCL modelC for the magic box scenario depicted in Fig. 25.3. As explained in the introduction, this scenario can be formalized with two contexts 1 and 2 that formalise the points of view ofMr. 1 andMr. 2, respectively. The two contexts are associated with two propositional logicsL ₁ andL ₂ respectively, defined over the sets of propositional atoms$\{l, r\}$ and$\{l, c, r\}$ ³. Intuitively, we aim at introducing a definition that says thatC satisfies the formula$1:\neg r \vee l$ as the two elementsc ₁ and$c' _1$ belonging to the (only) two chainsc and$c'$ in the modelC satisfy the formula$\neg r \vee l$ (where, in turn, the fact thatc ₁ and$c' _1$ satisfy$\neg r \vee l$ means that all the local models they contain satisfy that formula according to the notion of satisfiability in the appropriate logic, propositional in this case).

The above definition is sufficient for propositional contexts and also for quantificational contexts, if φ does not contain free variables. However, the general definition should also take into account the case in which φ containsfree and arrow variables, which need to be assigned to the elements of the domains of the models inc _i . Notice however the models ofc _i could have different domains of interpretation, so variables need to be assigned so that they are meaningful in all the models$m\in c_i$. i.e., to the intersections of the domains of the models inc _i . So ifa is an assignment for the variablex, since we want to maintain the definition that$c\models i:\phi(x)[a_i]$ if$m\models\phi(x)[a_i]$ for all$m\in c_i$, thenx should necessarily be assigned bya _i to some element which is in the intersection of the domains of each$m\in c_i$. More formally, alocal assignment a _i should map every (arrow) variablex in an element of$\bigcap_{m\in c_i}\Delta^m$, where Δ^m is the domain of interpretation associated to the modelm. We make the additional assumption that such an intersection is non-empty.

Formally, for any formula$i:\phi$, for every multi-context modelC, for every chain$c \in C$ and for every assignmenta _i that assigns the free variables occurring in$i:\phi$ to the intersection of the domains of interpretation of the locals models inc _i , we say that$C$ satisfies $i:\phi$ w.r.t. the assignmenta _i if for all$c\in C$,$c\models\phi[a_i]$, where$c\models\phi[a_i]$ means that$m \models_i\phi[a_i]$ for all the local modelsm of the i-th element$c_i \in c$, and ⊧ _i is the satisfiability relation defined in the logicL _i . We indicate thatC models$i:\phi$ with the symbol$C\models i:\phi[a_i]$. When we have to evaluate a set of labelled formulas Γ that span over multiple contexts free variables, as all the other symbols, are locally interpreted, and therefore we need to have an assignmenta _i for each context$i\in I$. This is calledlocal assignment. AnMC-assignment (or simply an assignment) is a family of assignments$a= \{a_i\}_{i\in I}$ such that for each$i\neq j\in I$,a _i assigns every variables ofL _i which is not an arrow variable, and ifL _i andL _j are quantificational logics, there is a domain relationr _ij such that: if$a_j(x^{i\rightarrow})$ is defined then$\left<a_i(x),a_j(x^{i\rightarrow})\right> \in r_{ij}$ and if$a_i(x^{\rightarrow j})$ is defined then$\left<a_i(x^{\rightarrow j}),a_j(x)\right> \in r_{ij}$.

2.5 Multi-context Logical Consequence

In MCL the notion of logical consequence is defined over labelled formulas. In particular, if Γ is a set of labelled formulas and$i:\phi$ a labelled formula, then$i:\phi$ is a logical consequence of Γ if and only if,

• 1. there is a modelC, a chain$c\in C$ and a family of assignments$a=\{a_i\}_{i\in I}$ to the free variables of$\Gamma\cup\{\phi\}$ such that$c\models\Gamma\cup\{i:\phi\}[a]$, and

• 2. for all modelsC, for all$c\in C$ and for all family of assignments$a=\{a_i\}_{i\in I}$ to the free variables of the formulas in Γ if$c\models\Gamma$ then there is an extension$a'$ of the assignmenta, to the free variables of φ such that$c\models i:\phi[a' _i]$ ⁴.

2.6 Information Flow Across Contexts via Bridge Rules

In a MCL every context is interpreted in a set of local models, possibly arranged into chains. Local interpretation is the way to relate the truth and the falsity of the formulas to each context. However, only certain combinations of local interpretations are possible. Those are the ones admitted by the class of compatibility relations associated to a MCL. At the level of formulas, this means that there is a dependency between the truth of a (set of) formulas in a context and the truth of different formulas another context. To go back to our magic box scenario, this means that if a formulal (there is a ball in the left sector) is true in the context of Mr.1, then the formula$l \vee c \vee r$ (there is at least one ball in the box) must be true in the context of Mr.2.

From this perspective we can say that (classes of) compatibility relation(s) determine an information flow across contexts: the truth of a certain formula in a context affects (imposes) the truth of another formula in a different context.Bridge rules are expressions over the languages of different contexts that enable the formalisation of this information flow. They are of the form:

$$i_1:\phi_1,\dots, i_n:\phi_n, \textsf{not}\ i_{n+1}:\phi_{n+1},\dots, \textsf{not}\ i_{m}:\phi_{m} \rightarrow i:\phi$$

(25.1)

with$0\leq n\leq m$,$i_k\in I$ and φ _k a formula in the language of$L_{i_k}$. The intuitive reading of (25.1) is: “if$\phi_1,\dots,\phi_n$ hold in$i_1,\dots,i_n$ respectively and$\phi_{n+1},\dots,\phi_{m}$ do not hold in$i_{n+1},\dots,i_m$ respectively, then φ holds ini.” Thus, a simple bridge rule that represents the propagation flow in the magic box example discussed above is

$$1:l \rightarrow 2:l \vee c \vee r.$$

(25.2)

2.7 Multi-context System

We are now ready to define an axiomatic system for multiple contexts. Amulti-context system MCS in a multi-context logic$L_I=\{L_i\}_{i\in I}$ is a pair$\left<\mathbb{T},\mathbb{BR}\right>$ where$\mathbb{T}$ is a family of theories$\{T_i\}_{i\in I}$, withT _i a set of closed formulas in the logicL _i , and$\mathbb{BR}$ is a set ofbridge rules. Intuitively, eachT _i axiomatizes what is true in the logicL _i , while the bridge rules$\mathbb{BR}$ axiomatize the constraints imposed by the compatibility relations and act like cross-logic axioms.

2.8 Reasoning in Multi-context Systems

There are multiple reasoning systems for MCL. Depending on the local logics, different reasoning systems have been developed in the past. Often, reasoning methods for specific MCL are the result of the combination via bridge rules of local reasoning methods. The work in Giunchiglia and Serafini (1994), Ghidini and Serafini (1998) propose an extension of Natural Deduction for reasoning in propositional and first order MCLs; in Serafiniand Roelofsen (2005) the SAT decision procedure for propositional logic is extended to a context SAT (or C-SAT) procedure to check for satisfiability in propositional multi-context systems; in Ghidini (1999), Borgida and Serafini (2003) tableaux methods for reasoning in modal and description logics have been extended for MCLs based on modal/description logics; Brewka et al. (2007) extends answer set programming to deal with propositional MCLs with non-monotonic bridge rules; finally, Bozzato and Serafini (2013) shows how SROIQ2-RL rule based forward reasoning can be extended to deal with multi-context logics in which each context is associated to a semantic web language OWL2RL. In the remaining of the chapter we will briefly recall and describe the most important reasoning methods that have been developed for MCLs along with an explanation of their main usages.

2.9 Local and Global Inconsistency

The fact that in MCL knowledge is split in multiple theories, makes MCL a flexible framework for modelling various types of inconsistencies. A first form of inconsistency arise when a proposition is assumed to hold in a context and the negation of the same proposition is assumed to hold in another context. This is easily represented in MCL with the two formulas$i:\phi$ and$j:\neg\phi$, which, in general, can be managed without generating any form of inconsistency. This is similar to what happens in multi modal logic where the two propositions$\Box_i\phi$ and$\Box_j\phi$ do not interfere, unless there are specific axioms that connect the two modalities φ _i and φ _j . In addition to this, in MCL we can define two forms of inconsistency. One is calledlocal inconsistency and refers to the fact that in a particular context it is possible to derive contradictory statements, i.e.,for some $i\in I$,$i:\phi$ and$i:\neg\phi$ are both derivable; the second is calledglobal inconsistency, which refers to the fact that a contradiction is derivable in all the contexts, i.e.,for all $i\in I$,$i:\phi$ and$i:\neg\phi$ are both derivable. In general local inconsistency does not entail global inconsistency. So it is possible that one context is locally inconsistent, while others are consistent. From the semantic perspective, local inconsistency in a contexti corresponds to the fact that there are chains in the compatibility relation of an MCL wherei is interpreted in the empty set of local model, while other contexts are associated with a non empty set of local models.

3 Propositional Multi-context Logic

The fisrt, and simplest, family of MCLs that was developed is based on an unstructured setI of contexts, where each context is described by means of a propositional logical language. Following the general definition, apropositional multi-context logic (PMCL) is defined starting from a family$\{P_i\}_{i\in I}$, where eachP _i is a set of propositional variables. Each logicL _i is therefore described using a propositional language defined onP _i . A model (compatibility relation)C for PMCL is composed by a set of chains$c\in C$ where eachc _i is a set of truth assignments to the propositional variables inP _i (that is, eachc _i is a set of propositional models defined overP _i ). Depending on the constraints one imposes onC it is possible to define various types of PMCS. In the following we provide three important examples of PMCS present in literature.

3.1 Partitioning Propositional Theories

One of the simplest ways of looking at multi-context logics is in terms of a partition of a (propositional) theory into a set of interactingmicrotheories. In this case the entire MCS is the (propositional) theory, the different contexts are the microtheories, and the compatibility relations (or analogously bridge rules) express the way microtheories are connected one to another. As explained in Amir and Mcilraith (2000), one of the main reason for partitioning a large (propositional) theory into a set of smaller interacting microtheories is efficiency of reasoning.

Partitioned propositional theories correspond to aspecific class of compatibility relations for PMCL, which we indicate withC _part , that contain chainsc defined as follows:

$$\begin{aligned}\text{for all} i\in I, & |c_i|=1\end{aligned}$$

(25.3)

$$\begin{aligned} \text{for all} p\in P_i\cap P_j, &c_i(p)=c_j(p)\end{aligned}$$

(25.4)

Condition (25.3) states that all the elementsc _i of a chain contain exactly one local model and intuitively represents the fact that each chain can be considered as composed of different contexts (the differentc _i ) that have acomplete representation of a scenario (from their point of view). For instance, the chain$c'=\langle{c' _1,c' _2}\rangle$ in Fig. 25.3 satisfies this requirement and correspond to the scenario in whichMr. 1 sees a ball in the left sector, and no ball in the right sector, andMr. 2 sees a ball in the center and left sectors and no ball in the right sector. Condition (25.4) states that the different elementsc _i contained in a chain agree on the interpretation of the propositional variables that are common to the two elements. Intuitively this means that the two contexts described by, say,$c_i \text{and} c_j$ agree on the truth value of the knowledge they have in common.

If we denote with$\models_{part}$ the logical consequence defined w.r.t.C _part , then we can state the following correspondence between a partitioned PMCL and propositional logic.

Theorem 1

Let $T= T_1uplus dotsuplus</Emphasis> </Para> <Para> <Emphasis Type="Italic">T_n$ be a propositional theory on the set of propositions P , which is partitioned in n theories $T_i\subseteq T$ (for $1\leq i\leq n$ ) defined on the set of propositional variables P _i , then: for every formula φ that contains only propositions in P _i , we have that

$$T\models \phi \mbox{if and only if} 1:T_1,\dots,n:T_n\models_{part} i:\phi.$$

3.2 Partial Views

Relaxing conditions (25.3) and (25.4) enables to obtain a more general (that is, weaker) class of MCLs where each context can be considered as describing a partial view on the world. For example, in Fig. 25.3 elementc ₁ corresponds to a partial view of the two sector’s box whereMr. 1 can state that there is a ball in the right sector but is uncommitted on whether there is a ball in the left hand side sector (e.g., because the sector is behind a wall as in an example shown in Ghidini and Giunchiglia (2001).

As shown in Roelofsen and Serafini (2004), this general formulation of PMCL is embeddable in the propositional multi-modal logic S5, with one modal operator φ _i for each context label$i\in I$. Local formulas of the form$i:\phi$ are translated in$\Box_i\phi$, and bridge rules of the form (25.1) are translated in the implication

$$\Box_{i_1}\phi_1\wedge\dots\wedge\Box_{i_n}\phi_{n}\rightarrow\Box_i\phi$$

(25.5)

{The correspondence between this PMCL and multi-modal S5 is not an equivalence since modal logics has aglobal language allowing formulas that express relations between local models which are more complex that the one representable in terms of propagation rules. For instance the modal formula$\Box_i\phi\vee\Box_j\phi$ does not correspond to any bridge rule betweeni andj as it cannot be represented as a propagation pattern. Another example is negated modal formulas like e.g.,$\neg\Box_i\phi$, which is not expressible in MCL, as it states that a proposition does not hold in a context. This limitations in the expressivity reflects the fundamental assumption of MCL, i.e., that every formula should be stated in a context. This expressivity limitation turns out to be of great help in the definition of modular reasoning systems, since they prevent to express global inconsistency, since there is no global formula. The assumption of not permitting global logical operators, has been relaxed in the formulaization of non-monotonic MCL (Brewka et al.2007), where the negation (as failure) operator is applicable to a labelled formula, obtaining$\mathbf{not}(i:\phi)$.}

3.3 Hierarchical Meta Logics

In the work on propositional multi-context logics, a special effort was devoted to investigate the usage of these formalisms to formalize the “object and meta relation” between contexts, that is, the situation in which for each context one can define a meta context that predicates on what holds in the object context.

Fig. 25.4

A hierarchical meta structure

In this caseI is the set of natural numbers with the usual total linear order, and each languageL _i is a propositional language, such that for every formula φ in the language ofL _i there is a propositional variable$\bullet(\phi)$ in the language of$L_{i+1}$, as depicted in Fig. 25.4.

The compatibility relationC _OM for a hierarchical meta logic satisfies the following constraints:

• 1. Closure w.r.t. union: If$c,c'\in C$, then$c\cup c'\in C$ (where$c\cup c'=\{c_i\cup c' _i\}_{i\in I}$).

• 2. Interpretation of meta-formulas: For all$c\in C$,$i\in I$ and φ inL _i ,$c_{i}\models\phi$ if and only if$c_{i+1}\models \bullet(\phi)$.

The work in Giunchiglia and Serafini (1994) shows that this logic is equivalent to the modal logic K, when the “•” operator is translated in the modal operator φ, while further works (see, e.g., Ghidini1999) prove that by further restrictingC it is possible to obtain the other normal modal logics, such as B, K4, K45, S4 and S5, and have applied these equivalence results to model propositional attitudes and multi-agent systems by means of a context-based approach (see, e.g., Cimatti et al.1994; Benerecetti et al.(1998a); Benerecetti et al.(1998b); Fisherand Ghidini2010).

4 Quantified Multi-context Logics

Quantified multi-context logics extend propositional MCL with the possibility of predicating object properties in different contexts and relations between objects. The two principles of MCL of locality and compatibility are extended to the contextual interpretation of terms. In details: according to the locality principle, each context is associated with a local domain. According to the compatibility principle, only certain combinations of local domains are admitted. For instance, ifA andB are the contexts associated to two databases DB$_A$ and DB$_B$, respectively, then the universe ofA (i.e., the set of constants that appear in the relations of DB$_A$) can be completely distinct from the universe of DB$_B$. For instance, the two databases might use different identifiers, and different ways to denote attributes, and so on. On the other hand, if the intended domains of both DB$_A$ and DB$_B$ overlap, i.e., they contain information about a common subset of objects, say books, then the identifiers of books used in the two databases should be somehow related. As explained in the introductory section, the relation between local domains is modelled via the, so-called, domain relation.

Specific instances of quantified MCL have been developed with the scope of formalizing heterogeneous database integration, ontology integration, and ontology matching. They are all monotonic logics, and the local logics are either first order logic, or description logics. In the following subsections we introduce the two main quantified MCLs: Distributed First Order Logics (Ghidini and Serafini1998) and Distributed Description Logics (Borgida and Serafini2003).

4.1 Distributed First Order Logics

DFOL is a family of MCL that has been defined with the objective of formalizing contextual knowledge expressed in first order languages. One of the main motivation for DFOL is the formalization of heterogeneous relational database integration (Serafini and Ghidini2004) and to provide a formal semantics for heterogeneous schema and ontology mapping (Serafini et al.2007).

A DFOL is defined on a family of first order logics$\{L_i\}_{i\in I}$. A DFOL model is any compatibility relation$\{c\}$ composed of a single chainc wherec _i , for all$i\in I$ is a (possibly empty) set of interpretations ofL _i on the same domain$\Delta_i\neq\emptyset$. With respect of the original formalization described in Ghidini and Serafini (1998) we also admit the arrow variable$x^{i\rightarrow}$ and$x^{\rightarrow i}$ in the languageL _i and the domain relationr _ii . This results in a more uniform treatment.

Consequently, this simplify the general definition on assignment, as this implies that the intersection of the domains of all the local models associated to the contexti, is the same as the domain of each local model. The representational hypothesis which derives by assuming shared domain for all local models inc _i is the fact that at each context there iscomplete knowledge on the size of the local domain. Formally this corresponds to the fact that every formula φ that does not contain, constant symbols, functional symbols, and predicate symbols with the exception of the equality symbol, is such that$C\models i:\phi$ or$C\models i:\neg \phi$. i.e., all theith local models agree on the evaluation of φ⁵. Examples of such formulas, are the those that allow to state bounds on the dimension of the domain. as,$i:\forall x_0,\dots,x_{m} \bigvee_{0\leq i<j\leq m} x_i=x_j$, which states thatith domain contains at mostm elements, and$i:\exists x_1,\dots,x_{n} \bigwedge_{0\leq i<j\leq n} x_i\neq x_j$ that states thatith domain contains at leastn elements. The assumptions, of constant local domains does not imply full constant domains, i.e., the fact that every domain in every context has the same dimension. Indeed, for instance the set of labelled formulas$\{1:\forall xy.x=y,\ 2:\exists xy. x\neq y\}$ is satisfiable, and they state that the domain of context 1 contain one element and the domain of context 2 contains at least two elements.

DFOL is the first example of MCL described in this chapter where logical consequence relation involves the assignment to variables. Under the assumption of constant local domains, we can simplify the definition of logical consequence as follows:

$$\Gamma\models\phi \textrm{if for every chain c and every assignment a for all the variables in} \Gamma, \textrm{if} c\models\Gamma[a] \textrm{then there is an extension of} a \textrm{ to} a' \textrm{such that} c\models i:\phi[a'].$$

(25.6)

4.1.1 Representing Cross Domain Constraints in DFOL

In the general case, i.e., when no constraints are imposed on the compatibility relation, the logical consequences across contexts is extremely week, and it is such that$\Gamma_{\neq i}\models i:\phi$ iff$\models i:\phi$ (where$\Gamma_{\neq i}$ is a set of labelled formulas with index different fromi). As in all the other MCL’s, also in DFOL it is possible to impose restrictions on the compatibility relation and on the domain relation by means of bridge rules. In the following we present some of the properties involving quantificational contextual information that can be formalized by means of DFOL bridge rules:

Absolute names. In general, in different contexts a constant (or a term) can have different meanings, however, it is also possible that the meaning of a term in a context is related to the meaning of another term in another context. An extreme situation is when a constant is anabsolute/global name. I.e., a constant that have the same meaning in all the context. Absolute names can be modelled by imposing the following bridge rule to be valid for every$i,j\in I$.

$$i:\textsf{a}=x^{i\rightarrow} \ \ \ \ i:\textsf{a} = x \rightarrow j:x^{i\rightarrow} = \textsf{a} \ \ \ \ i:\textsf{a} = x^{\rightarrow i} \rightarrow j:x = \textsf{a}$$

(25.7)

The first of the above bridge rules imposes that the constant$\textsf{a}$ is interpreted in a unique element by all local model inc _i . Indeed ifc _i contains two modelsm and$m'$ that interpret$\textsf{a}$ in two different objects, then it is not possible that$m\models \textsf{a}=x^{i\rightarrow}[a]$ and$m'\models \textsf{a}=x^{i\rightarrow}[a]$, and therefore$c\not\models i:\textsf{a}=x^{i\rightarrow}$. The other two bridge rules in (25.7) do not impose thata is interpreted in the same object ini andj, since Δ _i and Δ _j can be different (possibly disjoint) domains, but they state that the interpretation of$\textsf{a}$ in contextsi andj corresponds via the translation defined by the domain relation among the domains of the two contexts. If the bridge rules in (25.7) are imposed for two individual constants$\textsf{a}$ and$\textsf{b}$ in the intersection of the languages ofL _i andL _j , then we have that the following logical consequences hold.

$$i:\textsf{a} \neq \textsf{b} \models j: \textsf{a}\neq \textsf{b} \ \ \ i:\textsf{a} = \textsf{b} \models j: \textsf{a} =\textsf{b}$$

Imposing bridge rules (25.7) on the set of constants contained in the intersection of the universes of two databases DB$_A$ and DB$_B$, corresponds to assume that the intersection of the universes of the two DBs are isomorphic, and therefore this allow to safely join informations about the intersected domain available in both DBs.

Constraints on the domain relation. Bridge rules can be used to formalize relations between domains in different contexts. For instance, in some situation it is useful to assume that the domains of two contexts (sayi andj) are isomorphic. This can be forced by the bridge rules

$$\rightarrow j:\exists y.y = x^{i\rightarrow} \ \ \ \ \rightarrow i:\exists y.y = x^{\rightarrow j} \ \ \ \ i:x^{\rightarrow j} =y^{\rightarrow j} \rightarrow j:x=y$$

The first two of the above bridge rules imposes that for every elementx of the domain of contexti, there is a corresponding element of the domain of contextj and, vice-versa for every element of the domain of contextj, there is a corresponding element of the domain of contexti. The third one states that the domain relation betweeni andj must be a function. In Ghidiniand Serafini (1998) we describe how many other properties can be formalised by bridge rules containing just the equality symbol and arrow variables.

Join among heterogeneous domains. Bridge rules can be used to express the fact that a certain knowledge in a database DB$_C$ can be obtained by joining the information available in two heterogeneous databases DB$_A$ and DB$_B$. As an example, suppose that we want to represent that the ternary relation$R(x,y,z)$ in the database DB$_C$ is obtained by a join between the relations$P(x,y)$ in DB$_A$, and$Q(y,z)$ in DB$_B$ over the argumenty. But we know that the three databases have three heterogeneous representation of the values in the attributes, and therefore before doing the join it is necessary to perform a translation. There are three possible ways to proceed,

• Translate the tuples ofP from DB$_A$ into the DB$_B$, do the join inB and translate the result intoC. This is represented by the bridge rules

  $$A:P(x,y),\ B:Q(y,z)\wedge y^{A\rightarrow}=y\wedge x^{A\rightarrow}=x \rightarrow C:R(x^{B\rightarrow},y^{B\rightarrow},z^{B\rightarrow})$$

• Do the same but starting form DB$_B$, joining in DB$_A$ and translating in DB$_C$, which is represented by the bridge rule:

  $$B:R(y,z),\ A:P(x,y)\wedge y^{B\rightarrow}=y\wedge z^{B\rightarrow}=z \rightarrow C:R(x^{A\rightarrow},y^{A\rightarrow},z^{A\rightarrow})$$

• or transfer the tuples ofP andQ into DB$_C$ and do the join there. This way of reasoning is represented by the bridge rule:

  $$A:P(x,y),\ B: Q(y,z),\ C:x=x^{A\rightarrow}\wedge y=y^{A\rightarrow}\wedge y=y^{B\rightarrow}\wedge z=z^{B\rightarrow}\rightarrow C:R(x,y,z)$$

4.1.2 Reasoning in DFOL

Being DFOL an extension of first order logic, reasoning in DFOL is an undecidable task but it is finitely axiomatizable. In Ghidini and Serafini (1998) we proposed a sound and complete Natural Deduction Calculus for DFOL logical consequence parametrized on a set of bridge rules \textsf{BR}. This calculus is sound and complete with respect to the class of DFOL models and the domain relations that satisfies the set of bridge rules \textsf{BR}. Natural Deduction systems for FOL is a set of inference rules, with an arbitrary (finite) number of premises and a single conclusion. A deduction of φ form a set of hypothesis$\phi_1,\dots,\phi_n$ is a tree rooted at φ, with leaves$\phi_1,\dots,\phi_n$, such that the father node is derived by applying an inference rule to it’s children. The extension of ND to DFOL with bridge rules \textsf{BR}, is obtained by composing local deductions via bridge rules. Informally, the bridge rule$i_1:\phi_1(x),\ i_2:\phi_2(y) \rightarrow i:\psi(x^{{i_1}\rightarrow},y^{{i_2}\rightarrow})$ allows to “plug in” a deduction in contexti ₁ the two deductions performed in contexti ₁ andi ₂ that infers the premises of the bridge rule. In Fig. 25.5 we provide a graphical representation of local inference composition and an example of a simple proof in DFOL.

Fig. 25.5

A DFOL proof

4.2 Distributed Description Logics

{DDL has been introduced in Borgida and Serafini (2003) as a variation of multi-context logic with the motivation of modeling ontology matching and integration by means of a formal logic. In DDL local logicsL _i ’s are description logics.} The starting point of ontology mapping is constituted by two (a set of) ontologies, usually called source and target ontology. Ontology matching algorithms provides a set of semantic matches that partially maps the elements of the source ontology into the “corresponding” elements of the target ontology⁶. Once a source ontology is semantically matched with a target ontology, and every heterogeneity in the representation of knowledge by the two ontologies has been resolved, the knowledge contained in the two ontologies can be integrated and combined in a unique (sometimes modular) knowledge base. In many cases ontology matches act as information channels that propagate knowledge from the source ontology to the target ontology that is extended with the additional information coming from the source ontology. This perspective of ontology matching/integration can be naturally represented in multi-context logic, using context based on description logic languages. In DDL each context represents an ontology and semantic matches between a source ontologyi and a target ontologyj are represented via bridge rules with premises ini and consequences inj. A contexti can contain concepts and role subsumptions, namely formulas of the form$i:C\sqsubseteq D$,$i:R\sqsubseteq S$, and assertions, namely statements of the form$i:C(a)$ and$i:R(a,b)$ whereC andD are concept expressions,R andS are role expressions anda andb are individuals. A model for DDL is the same as a DFOL model on the FOL translation of the description logic language (where concepts, are unary predicate, relation binary predicates, and individual constants stays the same) with the restriction that for every chainc, and every$i\in I$,$|c_i|\leq 1$. DDL bride rules are used to represent ontology matches, and they can be defined among concepts, roles and individuals. Heterogeneous bridge rules has also been introduced, which maps concepts to roles and viceversa (e.g., “wedding” to “is-married-to”), but for simplicity we only report homogeneous bridge rules here: Bridge rules between concepts and roles are of two forms

$$i:C\stackrel{\sqsubseteq}{\longrightarrow} j:D \ \ \ \ i:C\stackrel{sqsupseteq}{\longrightarrow} j:D$$

(25.8)

whereC andD are concept expressions inL _i andL _j respectively. The above bridge rules are satisfied by the DDL modelc if there is domain relationr _ij such that

$$r_{ij}(C^{c_i}) \subseteq D^{c_j} \ \ \ \ r_{ij}(C^{c_i}) \supseteq D^{c_j}$$

(25.9)

where$X^{c_i}$ is the extension of the conceptC in the unique model$m\in c_i$ or it is the empty set if$c_i=\emptyset$.

The intuitive meaning of DDL bridge rules can be easily induced from the satisfiability conditions (25.9). In particular the$\stackrel{\sqsubseteq}{\longrightarrow}$ bridge rule, states that the conceptC ini matches with some subconcept ofD inj. While the$\stackrel{sqsupseteq}{\longrightarrow}$ bridge rule states that the conceptC ini is mapped into some superconcept ofD inj. Analogous bridge rules can be defined among roles. Bridge rules among individuals are expressions of the form

$$i:a \stackrel{=}{\longrightarrow} j:b_1.$$

(25.10)

The bridge rule (25.10) is satisfied when$\left<a^{m_i},b^{m_j}\right>\in r_{ij}$ (wherem _i andm _j are local models inc _i andc _j respectively). The intuitive meaning of the bridge rule (25.10) is thatb is one of the possible translations inj ofa ini.

Similarly to what happens for DL, which is a fragment of FOL, DDL is a fragment of DFOL. Indeed a DDL can be rewritteng into a DFOL by applying the standard translation of DL into FOL for each of the formulas inL _i , and by translating the bridge rule (25.8) into the following DFOL bridge rules:

$$i:C(x^{\rightarrow j})\rightarrow j:D(x) \ \ \ \ j:D(x) \rightarrow i:C(x^{\rightarrow j})$$

(25.11)

and translating the individual bridge rule (25.10) into

$$i:x=a\rightarrow j:x^{i\rightarrow}=b.$$

(25.12)

The semantics of DDL bridge rules entails a form of information propagation between mapped ontologies. The papers Serafini et al. (2004), Serafiniand Tamilin (2005), Ghidini et al. (2007) investigate on the knowledge propagation patterns between a source and a target ontology mapped with a set of DDL bridge rules. A simple example of such a propagation pattern fromi toj induced by a pair of mappings fromi toj is described by the following sound inference:

$$\begin{array}{c} i:A\sqsubseteq B\ \ \ i:A\stackrel{sqsupseteq}{\longrightarrow} j:G \ \ \ i:B\stackrel{\sqsubseteq}{\longrightarrow} j:H \\ \hline j:G \sqsubseteq H\end{array}.$$

The above propagation pattern in true for any unrestricted domain relation. However in many cases it’s interesting to investigate on DDL models where the domain relation satisfies natural restriction, such as functionality or injectivity or compositionality. The more restricted the domain relation the more information is passed by the bridge rules. Detailed investigation of different propagation patterns depending on the restriction imposed on the domain relation are studied in Homola and Serafini (2010).

5 Conclusions

Research and implementation activities around multi context system has been carried out for the last 25 years with a number of significant results that include propositional MCLs, first order MCLs, description logics-based MCLs, and MCL for semantic web languages like RDF and OWL. The research activities have focused to the development of theoretical frameworks as well as a set of prototype implementations, among which DRAGO, a Distributed Reasoning Architecture for a set of ontology linked via ontology mappings (Serafini and Tamilin2005), and the Contextualized Knowledge Repository (Bozzato et al.2013), a system that extends standard RDF triple stores with the capability of reasoning with multiple RDF graphs (Contexts) linked via bridge rules.

A number of studies that compare multi context system with other logical formalism that support distributed knowledge representation have also been developed, and mappings between the different formalisms have been proposed. In particular Serafini and Bouquet (2000) presents a formal comparison between propositional MCL and the propositional logic of contexts based on modal logics proposed in Buvac and Mason (1993), while Brockmans et al. (2009) exploits DFOL for encoding and comparing several formalisms for ontology mappings.

In this chapter we have provided an overview of the main families of multi context logics (MCLs), a logical formalism that allow to integrate multiple logical theories (contexts) in a structure of inter-related contexts, a description of their main logical properties and an illustration of the types of applications they have been used for.