In the previous section, we demonstrated that FIS and RIS are useful formalisms for data repre-sentation. However, to represent and reason about knowledge extracted from information systems, we need a logical language. We have seen that decision logic (DL) can represent and reason about information in FIS (i.e. data tables).
Since relations can be seen as properties of pairs of objects, to reason about RIS, we need a language that can be interpreted in the domain of pairs of objects. Arrow logic (AL) language [61, 87] is designed to describe all things that may be represented in a picture by arrows. Therefore, it is an appropriate tool for reasoning about RIS.
To represent rules induced from an RIS, we propose arrow decision logic (ADL), derived by combining the main features of AL and DL. In this section, we introduce the syntax and semantics of ADL. The atomic formulas of ADL are the same as those in DL; while the formulas of ADL are interpreted with respect to each pair of objects, as in the pair frames of AL [61, 87].
4.3.1 Syntax and semantics of ADL
An atomic formula of ADL is a descriptor of the form (i, h), where i ∈ A, h ∈ Hi, A is a finite set of attribute symbols, and for each i ∈ A, Hi is a finite set of relational indicator symbols. In addition, the wffs of ADL are defined by the formation rules for AL, while the definition of derived connectives is the same as that in AL.
1A multi-set is a set in which a multiplicity of elements is allowed.
An interpretation of a given ADL is an RIS, Tr = (U, A, {Hi | i ∈ A}, {ri | i ∈ A}), which can be seen as a square model of AL. Thus, the wffs of ADL are evaluated in terms of a pair of objects. More precisely, the satisfaction of a wff with respect to a pair of objects (x, y) in Tr is defined as follows (again, we omit the subscript Tr):
1. (x, y) |= (i, h) iff ri(x, y) = h, 2. (x, y) |= δ iff x = y,
3. (x, y) |= ¬ϕ iff (x, y) 6|= ϕ,
4. (x, y) |= ϕ ∨ ψ iff (x, y) |= ϕ or (x, y) |= ψ, 5. (x, y) |= ⊗ϕ iff (y, x) |= ϕ,
6. (x, y) |= ϕ ◦ ψ iff there exists z such that (x, z) |= ϕ and (z, y) |= ψ.
Let Σ be a set of ADL wffs; then, we write (x, y) |= Σ if (x, y) |= ϕ for all ϕ ∈ Σ. Also, for a set of wffs, Σ, and a wff, ϕ, we say that ϕ is an ADL consequence of Σ, written as Σ |= ϕ, if for every interpretation Tr and x, y in the universe of Tr, (x, y) |= Σ implies (x, y) |= ϕ.
Example 4.7 Let us use a RIS to represent the social network shown in Figure 4.1. The RIS is characterized by Tr = (U, A, {Hi | i ∈ A}, {ri | i ∈ A}), where
• U = {x1, x2, x3, x4}
• A ={Fr (Friend), Re (Recommendation), Tr (Trust)},
• HFr = HTr = {0, 1}, HRe = {0, 1, 2, 3}, and
• ri is shown in the three tables of the Figure.
By using ADL semantics, we can see, for example,
(x1, x3) |= ((Fr, 1) ◦ (Re, 3)) ∧ (Tr, 1), and (x4, x2) |= ((Fr, 1) ◦ (Re, 2)) ∧ ¬(Tr, 1).
Also, we have the following formulas valid in the RIS:
• ((Fr, 1) ◦ (Re, 3)) −→ (Tr, 1), which means that if someone is strongly recommended by an agent’s friend(s), then the agent will trust him,
• (Fr, 1) −→ ⊗(Fr, 1) which means that friendship is symmetric, and
• (Fr, 1) −→ (Tr, 1) ∧ (⊗(Tr, 1)), which means that friends trust each other
Fr x1 x2 x3 x4
The ADL consequence relation can be axiomatized by integrating the axiomatization of AL and specific axioms of DL. As shown in [61, 87], the AL consequence relations with respect to full square models can not be finitely axiomatized by an orthodox derivation system. To develop a complete axiomatization of AL, an unorthodox inference rule based on a difference operator D is added to the AL derivation system. The use of such unorthodox rules was first proposed by Gabbay [25]. The operator is defined in shorthand as follows:
Dϕ = > ◦ ϕ ◦ ¬δ ∨ ¬δ ◦ ϕ ◦ >,
where > denotes any tautology. According to the semantics, Dϕ is true in a pair (x, y) iff there exists a pair distinct from (x, y) such that ϕ is true in that pair.
The complete axiomatization of ADL consequence relations is presented in Figure 4.2, where ϕ, ψ, ϕ0, ψ0, and χ are meta-variables denoting any wffs of ADL. The axiomatization consists of three parts: the propositional logic axioms; the DL and AL axioms; and the inference rules, including the classical Modus Ponens rule, the universal generalization rule for modal operators, and the unorthodox rule based on D. The operator D is also utilized in DL3 to spread the axioms DL1 and DL2 to all pairs of objects. DL3 thus plays a key role in the proof of the completeness
of the axiomatization. DL1 and DL2 are exactly the specific axioms of DL in [67]. An additional axiom
¬(i, h) ≡ _
h0∈Hi,h06=h
(i, h0)
is presented in [67], but it is redundant. The AL axioms and inference rules can be found in [61], where AL4 is split into two parts and an extra axiom
ϕ ◦ (ψ ◦ (δ ∧ χ)) ⊃ (ϕ ◦ ψ) ◦ (δ ∧ χ)
is given. The extra axiom is called the weak associativity axiom, since it is weaker than the associativity axiom AL5. We do not need such an axiom, as it is an instance of AL5. The only novel axiom in our system is DL3. Though it is classified as a DL axiom, it is actually a connecting axiom between DL and AL.
An ADL derivation is a finite sequence ϕ1, · · · , ϕnsuch that every ϕi is either an instance of an axiom or obtainable from ϕ1, · · · , ϕi−1by an inference rule. The last formula ϕn in a derivation is called an ADL theorem. A wff ϕ is derivable in ADL from a set of wffs Σ if there are ϕ1, . . . , ϕn in Σ such that (ϕ1∧ . . . ∧ ϕn) ⊃ ϕ is an ADL-theorem. We use ` ϕ to denote that ϕ is an ADL theorem and Σ ` ϕ to denote that ϕ is derivable in ADL from Σ. Also, we write Σ `AL ϕ if ϕ is derivable in ADL from Σ without using the DL axioms.
The next theorem shows that the axiomatic system is sound and complete with respect to the ADL consequence relations.
Theorem 4.3 For any set of ADL wffs Σ ∪ {ϕ}, we have Σ |= ϕ iff Σ ` ϕ.
Proof:
1. Soundness: To show that Σ ` ϕ implies Σ |= ϕ, it suffices to show that all ADL axioms are valid in any ADL interpretation and that the inference rules preserve validity. The fact that AL axioms are valid and the inference rules preserve validity follows from the soundness of AL, since any ADL interpretation is an instance of a square model. Furthermore, it is clear that DL axioms are valid in any ADL interpretation.
2. Completeness: To prove completeness, we first note that the set of instances of DL axioms is finite. Let us denote χ by the conjunction of all instances of DL axioms and χ0 by the conjunction of all instances of axioms DL1 and DL2. If Σ 6` ϕ, then Σ ∪ {χ} 6`AL ϕ. Thus, by the completeness of AL, we have a pair model M = (U × U, C, R, I, π) and x, y ∈ U such that (x, y) |=M Σ, (x, y) |=M χ, and (x, y) |=M ¬ϕ. Next, we show that M can be transformed into an ADL interpretation. From (x, y) |=M χ, we can derive (z, w) |=Mχ0 for all z, w ∈ U by DL3. Thus, for every z, w ∈ U and i ∈ A, there exists exactly one hi,z,w ∈ Hi such that (z, w) |=M (i, hi,z,w). Consequently, Tr = (U, A, {Hi | i ∈ A}, {ri | i ∈ A}), where ri(z, w) = hi,z,w for z, w ∈ U and i ∈ A, is an ADL interpretation such that (x, y) |=Tr Σ and (x, y) |=Tr ¬ϕ. Thus,Σ 6` ϕ implies Σ 6|= ϕ.