Keywords

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

Medical natural language statements uttered by physicians or other health professionals and found in medical examination letters are usually graded, i.e., are associated with a degree of uncertainty about the validity of a medical assessment. This uncertainty is often expressed through specific verbs, adverbs, adjectives, or even phrases in natural language which we will call gradation words (related to linguistic hedges); e.g., Dr. X suspects that Y suffers from Hepatitis or The patient probably has Hepatitis or (The diagnosis of) Hepatitis is confirmed. Our approach is clearly not restricted to medical statements, but is applicable to graded statements in general, e.g., in technical diagnosis (the engine is probably overheated) or in everyday conversation (I’m pretty sure that Joe has signed a contract with Foo Inc.), involving trust (I’m not an expert, but ...) which can be seen as the common case (contrary to true universal statements).

In this paper, we look into a representation of such graded statements by presenting a simple non-standard modal logic which comes with a small set of partially-ordered modal operators, directly associated with the words indicating the uncertainty and interpreted through confidence intervals in the model theory. Our interest in such a formalization is related to the use of OWL in our projects as the de facto standard for ontologies today and its weakness to represent and reason about assertional knowledge that is uncertain [16] or that changes over time [10]. There are two principled ways to address such a restriction: either by sticking with the existing formalism (viz., OWL) and trying to find an encoding that still enables some useful forms of reasoning [16]; or by deviating from a defined standard in order to arrive, at best, at an easier, intuitive, and less error-prone representation [10].

Here, we follow the latter avenue, but employ and extend the standard entailment rules from [7, 15, 18] for positive binary relation instances in RDFS and OWL towards modalized n-ary relation instances, including transaction time and negation. These entailment rules talk about, e.g., subsumption, class membership, or transitivity, and have been found useful in many applications. The proposed solution has been implemented for the binary relation case (extended triples: quintuples) in HFC [11], a forward chaining engine that builds Herbrand models which are compatible with the open-world view underlying OWL.

This paper extends [12, 14] by new material, addressing the temporal change of graded statements. We will introduce a special notion of transaction time [17] (the time period in which a database entry is valid), contrary to valid time which we have investigated in [10] for the non-modal case. Due to space restrictions, we let the interested reader refer to [12, 14] for more material that we can not cover here, viz., (i) more on implementing modal entailments in HFC, (ii) specialized custom entailments, (iii) further kinds of modals (dual, in-the-middle), and (iv) related work, including the relation to the normal modal logic K and to Subjective Logic [8].

2 OWL Vs Modal Representation

We note here that the names of our initial modal operators were inspired by the qualitative information parts of diagnostic statements from [16] as shown in Fig. 1.

Fig. 1.
figure 1

Schematic mappings of the qualitative information parts excluded (E), unlikely (U), not excluded (N), likely (L), and confirmed (C) to confidence intervals. Picture taken from [16].

These qualitative parts were used in medical statements about, e.g., liver inflammation with varying levels of detail [16] in order to infer, e.g., if Hepatitis is confirmed then Hepatitis is likely but not Hepatitis is unlikely. And if Viral Hepatitis B is confirmed, then both Viral Hepatitis is confirmed and Hepatitis is confirmed (generalization). Things “turn around” when we look at the adjectival modifiers excluded and unlikely: if Hepatitis is excluded then Hepatitis is unlikely, but not Hepatitis is not excluded. Furthermore, if Hepatitis is excluded, then both Viral Hepatitis is excluded and Viral Hepatitis B is excluded (specialization).

[16] consider five OWL encodings, from which only two were able to fully reproduce the plausible inferences for the above Hepatitis use case. The encodings in [16] were quite cumbersome as the primary interest was to stay within the limits of the underlying calculus. Besides coming up with complex encodings, only minor forms of reasoning were possible, viz., subsumption reasoning. Furthermore, each combination of disease and qualitative information part required a new OWL class definition/new class name, and there exist a lot of them! These disadvantages are a result of two conscious decisions: OWL only provides unary and binary relations (concepts and roles) and comes up with a (mostly) fixed set of entailment/tableaux rules.

In our approach, however, the qualitative information parts from Fig. 1 are first class citizens of the object language (the modal operators) and diagnostic statements from the Hepatitis use case are expressed through the binary property suffersForm between p (patients, people) and d (diseases, diagnoses). The plausible inferences are then simply a byproduct of the instantiation of the entailment rule schemas (G) from Sect. 5.1, and (S1) and (S0) from Sect. 5.2 for property suffersForm (the rule variables are universally quantified; \(\top \) = universal truth; C = confirmed; L = likely), e.g.,

   (S1) \(\mathsf{ViralHepatitisB} \sqsubseteq \mathsf{ViralHepatitis} \wedge \mathsf{ViralHepatitisB}(d)\)

         \(\rightarrow \top \mathsf{ViralHepatitis}(d)\)

   (G) \(C \mathsf{suffersFrom}(p, d) \rightarrow L \mathsf{suffersFrom}(p, d) \)

Two things are worth mentioning here. Firstly, not only OWL properties can be graded, such as \(C \mathsf{suffersFrom}(p, d)\) (= it is confirmed that p suffers from d), but also class membership, e.g., \(C \mathsf{ViralHepatitisB}(d)\) (= it is confirmed that d is of type Viral Hepatitis B). As the original OWL example from [16] can not make use of any modals, we employ the special modal \(\top \) here: \(\top \mathsf{ViralHepatitisB}(d)\). Secondly, modal operators are only applied to assertional knowledge (the ABox in OWL)—neither TBox nor RBox axioms are being affected by modals in our approach, as they are supposed to express universal truth.

3 Confidence and Confidence Intervals

We address the confidence of an asserted (medical) statement [16] through graded modalities applied to propositional formulae: E (excluded), U (unlikely), N (not excluded), L (likely), and C (confirmed). For various (technical) reasons, we add a wildcard modality ? (unknown), a complementary failure modality ! (error), plus two further modalities to syntactically state definite truth and falsity: \(\top \) (true, or top) and \(\bot \) (false or bottom).Footnote 1 Let \(\triangle \) now denotes the set of all modalities: \(\triangle := \{?, !, \top , \bot , E, U, N, L, C\}\).

A measure function \(\mu : \triangle \mapsto [0,1] \times [0,1]\) is a mapping which returns the associated confidence interval \(\mu (\delta ) = [l, h]\) for a modality from \(\delta \in \triangle \) (\(l \le h\)). We write \(||\delta || = h - l\) to denote the length of the confidence interval and presuppose that \(\mu (?) = [0, 1]\), \(\mu (\top ) = [1, 1]\), \(\mu (\bot ) = [0, 0]\), and \(\mu (!) = \emptyset \).Footnote 2

In addition, we define two disjoint subsets of \(\triangle \), called and and again make a presupposition: the confidence intervals for modals from end in 1, whereas the confidence intervals for modals always start with 0. It is worth noting that we do not make use of \(\mu \) in the syntax of the modal language (for which we employ the modalities from \(\triangle \)), but in the semantics when dealing with the satisfaction relation of the model theory (see Sect. 4).

We have talked about confidence intervals now several times without saying what we actually mean by this. Suppose that a physician says that it is confirmed (= C) that patient p suffers from disease d, for a set of observed symptoms (or evidence) \(S = \{S_1, \ldots , S_k\}\): \(C { suffersFrom}(p, d)\).

Assuming that a different patient \(p^\prime \) shows the same symptoms S (and only S, and perhaps further symptoms which are, however, independent from S), we would assume that the same doctor would diagnose \(C { suffersFrom}(p^\prime , d)\).

Even an other, but similar trained physician is supposed to grade the two patients similarly. This similarity which originates from patients showing the same symptoms and from physicians being taught at the same medical school is addressed by confidence intervals and not through a single (posterior) probability, as there are still variations in diagnostic capacity and daily mental state of the physician. By using intervals (instead of single values), we can usually reach a consensus among people upon the meaning of gradation words, even though the low/high values of the confidence interval for, e.g., confirmed might depend on the context.

Being a bit more theoretic, we define a confidence interval as follows. Assume a Bernoulli experiment [9] that involves a large set of n patients P, sharing the same symptoms S. W.r.t. our example, we would like to know whether \({ suffersFrom}(p,d)\) or \(\lnot { suffersFrom}(p,d)\) is the case for every patient \(p \in P\), sharing S. Given a Bernoulli trials sequence \(\mathbf {X} = (X_1, \ldots , X_n)\) with indicator random variables \(X_i \in \{0, 1\}\) for a patient sequence \((p_1, \ldots , p_n)\), we can approximate the expected value E for \({ suffersFrom}\) being true, given disease d and background symptoms S by the arithmetic mean A: \(\text {E}[\mathbf {X}] \approx \text {A}[\mathbf {X}] = \frac{\sum _{i=1}^n X_i}{n}\).

Due to the law of large numbers, we expect that if the number of elements in a trials sequence goes to infinity, the arithmetic mean will coincide with the expected value: \(\text {E}[\mathbf {X}] = \lim _{n \rightarrow \infty } \frac{\sum _{i=1}^n X_i}{n}\).

Clearly, the arithmetic mean for each new finite trials sequence is different, but we can try to locate the expected value within an interval around the arithmetic mean: \(\text {E}[\mathbf {X}] \in [\text {A}[\mathbf {X}] - \epsilon _1, \text {A}[\mathbf {X}] + \epsilon _2]\). For the moment, we assume \(\epsilon _1 = \epsilon _2\), so that A\([\mathbf {X}]\) is in the center of this interval which we will call from now on confidence interval.

Coming back to our example and assuming \(\mu (C) = [0.9, 1]\), \(C { suffersFrom}(p, d)\) can be read as being true in 95% of all cases known to the physician, involving patients p potentially having disease d and sharing the same prior symptoms (evidence) \(S_1, \ldots , S_k\): \((\sum _{p \in P} \text {Prob}({ suffersFrom}(p, d) | S))/n \approx 0.95\).

The variance of \(\pm 5\%\) is related to varying diagnostic capabilities between (comparative) physicians, daily mental form, undiscovered important symptoms or examinations which have not been carried out (e.g., lab values), or perhaps even by the physical stature of the patient (crooked vs. upright) which unconsciously affects the final diagnosis, etc., as elaborated above. Thus the individual modals from \(\triangle \) express (via \(\mu \)) different forms of the physician’s confidence, depending on the set of already acquired symptoms as (potential) explanations for a specific disease.

4 Normal Form and Model Theory

Let \(\mathcal{C}\) denote the set of constants that serve as the arguments of a relation instance. For instance, in an RDF/OWL setting, \(\mathcal{C}\) would exclusively consist of XSD atoms, blank nodes, and URIs/IRIs. In order to define basic n-ary propositional formulae (ground atoms), let \(p(\mathbf {c})\) abbreviates \(p(c_1, \ldots , c_n)\), for \(c_1, \ldots , c_n \in C\), given \(\text {length}(\mathbf {c}) = n\). In case the number of arguments does not matter, we sometimes simply write p, instead of, e.g., p(cd) or \(p(\mathbf {c})\). As before, we assume \(\triangle = \{?, !, \top , \bot , E, U, N, L, C\}\). We inductively define the set of well-formed formulae \(\phi \) of our modal language as follows:

$$ \phi \,{:}{:=}\, p(\mathbf {c}) \mid \lnot \phi \mid \phi \wedge \phi ^\prime \mid \phi \vee \phi ^\prime \mid \triangle \phi $$

4.1 Simplification and Normal Form

We now syntactically simplify the set \(\Phi \) of well-formed formulae \(\phi \) by restricting the uses of negation and modalities to the level of propositional letters \(\pi \):

$$ \bullet \; \pi \,{:}{:=}\, p(\mathbf {c}) \mid \lnot p(\mathbf {c}) \bullet \; \phi \,{:}{:=}\, \pi \mid \triangle \pi \mid \phi \wedge \phi ^\prime \mid \phi \vee \phi ^\prime $$

The design of this language is driven by two main reasons: firstly, we want to effectively implement the logic (in our case, in HFC), and secondly, the application of the below semantic-preserving simplification rules in an offline pre-processing step makes the implementation easier and guarantees a more efficient runtime system. To address negation, we first need the notion of a complement modal \(\delta ^\mathsf{C}\) for every \(\delta \in \triangle \), where

$$ \mu (\delta ^\mathsf{C}) := {\mu (\delta )}^\mathsf{C} = \mu (?) \setminus \mu (\delta ) = [0, 1] \setminus \mu (\delta ) $$

I.e., \(\mu (\delta ^\mathsf{C})\) is defined as the complementary interval of \(\mu (\delta )\) (within the bounds of [0, 1], of course). For example, E and N (excluded, not excluded) or ? and ! (unknown, error) are already existing complementary modals.

We also require mirror modals \(\delta ^\mathsf{M}\) for every \(\delta \in \triangle \) whose confidence interval \(\mu (\delta ^\mathsf{M})\) is derived by “mirroring” \(\mu (\delta )\) to the opposite side of the confidence interval, either to the left or to the right:Footnote 3

$$ \mathbf{if} \; \mu (\delta ) = [l, h] \; \mathbf{then} \; \mu (\delta ^\mathsf{M}) := [1 - h, 1 - l] $$

For example, E and C (excluded, confirmed) or \(\top \) and \(\bot \) (top, bottom) are mirror modals. In order to transform \(\phi \) into its negation normal form, we need to apply simplification rules a finite number of times (until rules are no longer applicable). We depict those rules by using the \(\vdash \) relation, read as formula \(\vdash \) simplified formula (\(\epsilon \) = empty word):

  1. 1.

    \(? \phi \vdash \epsilon \)                     (\(? \phi \) is not informative at all)

  2. 2.

    \(\lnot \lnot \phi \vdash \phi \)

  3. 3.

    \(\lnot (\phi \wedge \phi ^\prime ) \vdash \lnot \phi \vee \lnot \phi ^\prime \)

  4. 4.

    \(\lnot (\phi \vee \phi ^\prime ) \vdash \lnot \phi \wedge \lnot \phi ^\prime \)

  5. 5.

    \(\lnot \triangle \phi \vdash \triangle ^\mathsf{C} \phi \)              (example: \(\lnot E \phi = E^\mathsf{C} \phi = N \phi \))

  6. 6.

    \(\triangle \lnot \phi \vdash \triangle ^\mathsf{M} \phi \)              (example: \(E \lnot \phi = E^\mathsf{M} \phi = C \phi \))

Clearly, the mirror modals \(\delta ^\mathsf{M}\) (\(\delta \in \triangle \)) are not necessary as long as we explicitly allow for negated statements (which we do), and thus case 6 can, in principle, be dropped.

What is the result of simplifying \(\triangle (\phi \wedge \phi ^\prime )\) and \(\triangle (\phi \vee \phi ^\prime )\)? Let us start with the former case and consider as an example the statement about an engine that a mechanical failure m and an electrical failure e is confirmed: \(C (m \wedge e)\). It seems plausible to simplify this expression to \(C m \wedge C e\). Commonsense tells us furthermore that neither Em nor Ee is compatible with this description (we should be alarmed if, e.g., both Cm and Em happen to be the case).

Now consider the “opposite” statement \(E (m\,\wedge \,e)\) which must not be rewritten to \(E m \wedge E e\), as either Cm or Ce is well compatible with \(E (m \wedge e)\). Instead, we rewrite this kind of “negated” statement as \(E m \vee E e\), and this works fine with either Cm or Ce.

In order to address the other modal operators, we generalize these plausible inferences by making a distinction between and modals (cf. Sect. 3):

figure a

Let us now focus on disjunction inside the scope of a modal operator. As we do allow for the full set of Boolean operators, we are allowed to deduce

  1. 8.

    \(\triangle (\phi \vee \phi ^\prime ) \vdash \triangle (\lnot (\lnot (\phi \vee \phi ^\prime ))) \vdash \triangle (\lnot (\lnot \phi \wedge \lnot \phi ^\prime )) \vdash \triangle ^\mathsf{M} (\lnot \phi \wedge \lnot \phi ^\prime )\)

This is, again, a conjunction, so we apply schemas 7a and 7b, giving us

figure b

Note how the modals from in 7a and 8a act as a kind of negation operator to turn the logical operators into their counterparts, similar to de Morgan’s law.

The final case considers two consecutive modals:

  1. 9.

    \(\delta _1 \delta _2 \phi \vdash (\delta _1 \circ \delta _2) \phi \)

We interpret the \(\circ \) operator as a kind of function composition, leading to a new modal \(\delta \) which is the result of \(\delta _1 \circ \delta _2\). We take a liberal stance here of what the result is, but indicate that it depends on the domain and, again, plausible inferences we like to capture. The \(\circ \) operator will probably be different from the related operation \(\odot \) which is used in Sect. 5.3.

4.2 Model Theory

In the following, we extend the standard definition of modal (Kripke) frames and models [3] for graded modal operators from \(\triangle \) by employing the confidence function \(\mu \) and focussing on the minimal definition for \(\phi \). A frame \(\mathcal{F}\) for the probabilistic modal language is a pair \(\mathcal{F} = \langle \mathcal{W}, \mathcal{R}_\triangle \rangle \) where \(\mathcal{W}\) is a non-empty set of worlds (or situations, states, points, vertices, etc.) and \(\mathcal{R}_\triangle \) a family of binary relations over \(\mathcal{W} \times \mathcal{W}\), called accessibility relations. In the following, we write \(R_\delta \) to depict the accessibility relation for modal \(\delta \in \triangle \).

A model \(\mathcal{M}\) for the probabilistic modal language is a triple \(\mathcal{M} = \langle \mathcal{F}, \mathcal{V}, \mu \rangle \), such that \(\mathcal{F}\) is a frame, \(\mathcal{V}: \Phi \mapsto 2^\mathcal{W}\) is a valuation, assigning each proposition \(\phi \in \Phi \) a subset of \(\mathcal{W}\), viz., the set of worlds in which \(\phi \) holds, and \(\mu \) is a mapping, returning the confidence interval for a given modality from \(\triangle \). Note that we only require a definition for \(\mu \) in \(\mathcal{M}\) (the model, but not in the frame), as \(\mathcal{F}\) represents the relational structure without interpreting the edge labelling \(R_\delta \) of the graph.

The satisfaction relation \(\models \), given a model \(\mathcal{M}\) and a specific world w is inductively defined over the set of well-formed formulae in negation normal form (remember \(\pi \,{:}{:=}\, p(\mathbf {c}) \mid \lnot p(\mathbf {c})\)):

  1. 1.

    \(\mathcal{M}, w \models p(\mathbf {c})\)  iff  \(w \in \mathcal{V}(p(\mathbf {c}))\) and \(w \not \in \mathcal{V}(\lnot p(\mathbf {c}))\)

  2. 2.

    \(\mathcal{M}, w \models \lnot p(\mathbf {c})\)  iff  \(w \in \mathcal{V}(\lnot p(\mathbf {c}))\) and \(w \not \in \mathcal{V}(p(\mathbf {c}))\)

  3. 3.

    \(\mathcal{M}, w \models \phi \wedge \phi ^\prime \)  iff  \(\mathcal{M}, w \models \phi \) and \(\mathcal{M}, w \models \phi ^\prime \)

  4. 4.

    \(\mathcal{M}, w \models \phi \vee \phi ^\prime \)  iff  \(\mathcal{M}, w \models \phi \) or \(\mathcal{M}, w \models \phi ^\prime \)

  5. 5.

    for all \(\delta \in \underline{1}\): \(\mathcal{M}, w \models \delta \pi \)  iff  \(\frac{\#\,\{u \mid (w, u) \in R_\delta \;{\mathbf{and}}\; \mathcal{M}, u \models \pi \}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

  6. 6.

    for all \(\delta \in \underline{0}\): \(\mathcal{M}, w \models \delta \pi \)  iff  \(1 - \frac{\#\,\{u \mid (w, u) \in R_\delta \;{\mathbf{and}}\; \mathcal{M}, u \models \pi \}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

The last two cases of the satisfaction relation addresses the modals: for a world w, we look for the successor states u that are directly reachable via \(R_\delta \) and in which \(\pi \) holds, and divide the number of such states (\(\#\,\cdot \)) by the number of all worlds that are reachable from w by an arbitrary \(R_{\delta ^\prime }\) in the denominator. This number, lying between 0 and 1, is then required to be an element of the confidence interval \(\mu (\delta )\) of \(\delta \), in case \(\delta \in \underline{1}\). For the modals whose confidence intervals start at 0, we clearly need to subtract this number from 1.

It is worth noting that the satisfaction relation above differs from the standard definition in its handling of \(\mathcal{M}, w \models \lnot p(\mathbf {c})\), as negation is not interpreted through the absence of \(p(\mathbf {c})\) (\(\mathcal{M}, w \not \models p(\mathbf {c})\)), but through the existence of \(\lnot p(\mathbf {c})\). This treatment addresses the open-world nature in OWL and the evolvement of a (medical) domain over time.

We also note that the definition of the satisfaction relation for modalities (last clause) is related to the possibility operators \(M_k \cdot \) (= \(\Diamond ^{\ge k} \cdot \); \(k \in \mathbb {N}\)) introduced by [5] and counting modalities \(\cdot \ge n\) [1], used in modal logic characterizations of description logics with cardinality restrictions.

4.3 Two Constraints: Well-Behaved Frames

The definition of the satisfaction relation \(\models \) above makes no assumptions about the underlying frame \(\mathcal{F}\). For various reasons described below, we will now impose two constraints \((\mathcal{C}_1)\) and \((\mathcal{C}_2)\) on \(\mathcal{F}\).

As we will see later, it is handy to assume that the graded modals are arranged in a kind of hierarchy—the more we move along the arrows in the hierarchy, the more a statement \(\phi \) in the scope of a modal \(\delta \in \triangle \) becomes uncertain. In order to address this, we slightly extend the notion of a frame by a third component \({\preceq } \subseteq \triangle \times \triangle \), a partial order (i.e., a reflexive, antisymmetric, and transitive binary relation) between modalities: \(\mathcal{F} = \langle \mathcal{W}, \mathcal{R}_\triangle , \preceq \rangle \).

Let us consider the following modal hierarchy that we build from the set \(\triangle \) of already introduced modals (cf. Fig. 1):

figure c

This graphical representation is just a compact way to specify a set of 33 binary relation instances over \(\triangle \times \triangle \), such as \(\top \preceq \top \), \(\top \preceq N\), \(C \preceq N\), \(\bot \preceq {?}\), or \(! \preceq {?}\). The above mentioned form of uncertainty is expressed by the measure function \(\mu \) in that the associated confidence intervals become larger:

$$ \mathbf{if} \; \delta \preceq \delta ^\prime \; \mathbf{then} \; \mu (\delta ) \subseteq \mu (\delta ^\prime ) $$

In order to arrive at a proper and intuitive model-theoretic semantics which mirrors intuitions such as if \(\phi \) is confirmed (\(C \phi \)) then \(\phi \) is likely (\(L \phi \)), we will focus here on well-behaved frames \(\mathcal{F}\) which enforce the existence of edges in \(\mathcal{W}\), given \(\preceq \) and \(\delta , \delta ^\uparrow \in \triangle \):

$$ \begin{array}{ll} (\mathcal{C}_1) &{} \mathbf{if} \; (w, u) \in R_\delta \; \mathbf{and} \; \delta \preceq \delta ^\uparrow \\ &{} \mathbf{then} \; (w, u) \in R_{\delta ^\uparrow } \end{array} $$

However, by imposing this constraint, we also need to adapt the last two cases of the satisfiability relation from Sect. 4.2:

  1. 5.

    for all \(\delta \in \underline{1}\): \(\mathcal{M}, w \models \delta \pi \) iff  \(\frac{\#\,\cup _{\delta ^\uparrow \succeq \delta }\{u \mid (w, u) \in R_{\delta ^\uparrow } \;{ \mathbf{and}}\; \mathcal{M}, u \models \pi \}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

  2. 6.

    for all \(\delta \in \underline{0}\): \(\mathcal{M}, w \models \delta \pi \) iff  \(1 - \frac{\#\,\cup _{\delta ^\uparrow \succeq \delta }\{u \mid (w, u) \in R_{\delta ^\uparrow } \;{ \mathbf{and}}\; \mathcal{M}, u \models \pi \}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

Not only are we scanning for edges (wu) labeled with \(R_\delta \) and for successor states u of w in which \(\pi \) holds in the numerator (original definition), but also take into account edges \(R_{\delta ^\uparrow }\) marked with more general modals \(\delta ^\uparrow \), given \(\delta ^\uparrow \succeq \delta \). This mechanism implements a kind of built-in model completion that is not necessary in ordinary modal logics as they deal with only a single relation (viz., unlabelled arcs).

We have also seen that negated propositions inside the scope of a modal can be formulated equivalently by using the mirror modal: \(\delta \lnot \phi \equiv \delta ^\mathsf{M} \phi \). Since \(\mathcal{F}\) is only constrained by \((\mathcal{C}_1)\) so far, we impose a further restriction to guarantee that the satisfaction relation works properly for the interplay between negation and mirror modals as otherwise the fraction in case (5) will yield wrong numbers. In order to capture both the left-to-right and the right-to-left direction of the equivalence, we use \(\pi \) here for abbreviating the propositional letters \(\pi \,{:}{:=}\, p(\mathbf {c}) \mid \lnot p(\mathbf {c})\) (see Sect. 4.1):

$$ \begin{array}{ll} (\mathcal{C}_2) &{} \mathbf{if} \; (w, u) \in R_\delta \; \mathbf{s.t.} \; u \in \mathcal{V}(\lnot \pi ) \\ &{} \mathbf{then} \; \exists u^\prime \in \mathcal{W} \; \mathbf{s.t.} \; (w, u^\prime ) \in R_{\delta ^\mathsf{M}} \; \mathbf{and} \; u^\prime \in \mathcal{V}(\pi ) \end{array} $$

5 Entailment Rules

We now turn our attention, again, to the syntax of our language and to the syntactic consequence relation. This section addresses a restricted subset of entailment rules which will unveil new (or implicit) knowledge from already existing graded statements. Recall that these kind of statements (in negation normal form) are a consequence of the application of simplification rules as depicted in Sect. 4.1. Thus, we assume a pre-processing step here that “massages” more complex statements that arise from a representation of graded (medical) statements in natural language. The entailments which we will present in a moment can either be directly implemented in a tuple-based reasoner, such as HFC [11], or in triple-based engines (e.g., Jena [4] or OWLIM [2]) which need to reify the medical statements in order to be compliant with the RDF triple model.

5.1 Modal Entailments

The entailments presented in this section deal with plausible inference centered around modals \(\delta , \delta ^\prime \in \triangle \) which are, in part, also addressed in [16] in a pure OWL setting. We use the implication sign \(\rightarrow \) to depict the entailment rules \({ lhs} \rightarrow { rhs}\) which act as completion (or materialization) rules the way as described in, e.g., [7] and [18], and used in today’s semantic repositories (e.g., OWLIM). We sometimes even use the biconditional \(\leftrightarrow \) to address that the LHS and the RHS are semantically equivalent, but will indicate the direction that should be used in a practical setting. As before, we define \(\pi \,{:}{:=}\, p(\mathbf {c}) \mid \lnot p(\mathbf {c})\). We furthermore assume that for every modal \(\delta \in \triangle \), a complement modal \(\delta ^\mathsf{C}\) and a mirror modal \(\delta ^\mathsf{M}\) exist (cf. Sect. 4.1).

Lift . This rule interprets propositional statements as special modal formulae. It might be dropped and can be seen as a pre-processing step. We have used it in the Hepatitis example above. Usage: left-to-right direction.

Generalize \({}\). This rule schema can be instantiated in various ways, using the modal hierarchy from Sect. 4.3, e.g., \(\top \pi \rightarrow C \pi \), \(C \pi \rightarrow L \pi \), or \(E \pi \rightarrow U \pi \). It has been used in the Hepatitis example.

Complement . In principle, (C) is not needed in case the statement is already in negation normal form. This schema might be useful for natural language paraphrasing (explanation). Given \(\triangle \), there are four possible instantiations: \(E \pi \leftrightarrow \lnot N \pi \), \(N \pi \leftrightarrow \lnot E \pi \), \(? \pi \leftrightarrow \lnot ! \pi \), and \(! \pi \leftrightarrow \lnot ? \pi \).

Mirror . Again, (M) is in principle not needed as long as the modal proposition is in negation normal form, since we do allow for negated propositional statements \(\lnot p(\mathbf {c})\). This schema might be useful for natural language paraphrasing (explanation). For \(\triangle \), there are six possible instantiations: \(E \pi \leftrightarrow C \lnot \pi \), \(C \pi \leftrightarrow E \lnot \pi \), \(L \pi \leftrightarrow U \lnot \pi \), \(U \pi \leftrightarrow L \lnot \pi \), \(\top \pi \leftrightarrow \bot \lnot \pi \), and \(\bot \pi \leftrightarrow \top \lnot \pi \).

Uncertainty . The co-occurrence of \(\delta \pi \) and \(\lnot \delta \pi \) does not imply logical inconsistency (propositional case: \(\pi \wedge \lnot \pi \)), but leads to complete uncertainty about the validity of \(\pi \). Usage: left-to-right direction. Remember that \(\mu (?) = \mu (\delta ) \uplus \mu (\delta ^\mathsf{C}) = [0, 1]\):

figure d

Negation . (N) can be easily shown by applying the simplification rules from Sect. 4.1. \(\delta (\pi \wedge \lnot \pi )\) can be formulated equivalently by using the mirror modal \(\delta ^\mathsf{M}\):

figure e

In general, (N) is not the modal counterpart of the law of non-contradiction, as \(\pi \wedge \lnot \pi \) is usually afflicted by uncertainty, meaning that from \(\delta (\pi \wedge \lnot \pi )\), we can not infer that \(\pi \wedge \lnot \pi \) is the case for the concrete example in question (recall the intention behind the confidence intervals; cf. Sect. 3). There is one notable exception, involving the \(\top \) and \(\bot \) modals. This is formulated by the next entailment rule.

Error . (E) is the modal counterpart of the law of non-contradiction (note: \(\bot ^\mathsf{M} = \top , \top ^\mathsf{M} = \bot , {!^\mathsf{M}} = {!}\)). For this reason and by definition, the error (or failure) modal ! from Sect. 3 comes into play here. The modal ! can serve as a hint to either stop a computation the first time it occurs, or to continue reasoning and to syntactically memorize the ground literal \(\pi \). Usage: left-to-right direction.

5.2 Subsumption Entailments

As before, we define two subsets of \(\triangle \), called and , thus effectively become and due to the use of complement modals \(\delta ^\mathsf{C}\) and mirror modals \(\delta ^\mathsf{M}\) for every base modal \(\delta \in \triangle \) and by assuming that \(E = N^\mathsf{C}\), \(E = C^\mathsf{M}\), \(U = L^\mathsf{M}\), and \(\bot = \top ^\mathsf{M}\), together with the four “opposite” cases.

Now, let \(\sqsubseteq \) abbreviate relation subsumption as known from description logics and realized through subClassOf and subPropertyOf in RDFS. Given this, we define two further very practical and plausible modal entailments which can be seen as the modal extension of the entailment rules (rdfs9) and (rdfs7) for classes and properties in RDFS [7]:

figure f

Note how the use of p and q switches in the antecedent and the consequent, even though \(p \sqsubseteq q\) holds in both cases. Note further that propositional statements \(\pi \) are restricted to the positive case \(p(\mathbf {c})\) and \(q(\mathbf {c})\), as their negation in the antecedent will not lead to any valid entailments.

Here are two instantiations of (S0) and (S1) for the unary and binary case (remember, and ):

\( \mathsf{ViralHepatitis} \sqsubseteq \mathsf{Hepatitis} \wedge E \mathsf{Hepatitis}(x) \rightarrow E \mathsf{ViralHepatitis}(x)\)

\(\mathsf{deeplyEnclosedIn} \sqsubseteq \mathsf{containedIn} \wedge C \mathsf{deeplyEnclosedIn}(x, y) \rightarrow C \mathsf{containedIn}(x, y)\)

5.3 Extended RDFS and OWL Entailments

In this section, we will consider further entailment rules for RDFS [7] and a restricted subset of OWL [15, 18]. Remember that modals only head positive and negative propositional letters \(\pi \), not TBox or RBox axioms. Concerning the original entailment rules, we will distinguish four principal cases to which the extended rules belong (we will only consider the unary and binary case here as used in description logics/OWL):

  1. 1.

    TBox and RBox axiom schemas will not undergo a modal extension;

  2. 2.

    rules get extended in the antecedent;

  3. 3.

    rules take over modals from the antecedent to the consequent;

  4. 4.

    rules aggregate several modals from the antecedent in the consequent.

We will illustrate the individual cases in the following with examples by using a kind of description logic rule syntax. Clearly, the set of extended entailments depicted here is not complete.

Case-1: No Modals. Entailment rule (rdfs11) from [7] deals with class subsumption: \(\mathsf{C \sqsubseteq D \wedge D \sqsubseteq E \rightarrow C \sqsubseteq E}\). As this is a terminological axiom schema, the rule stays constant in the modal domain. Example rule instantiation:

\( \mathsf{ViralHepatitisB} \sqsubseteq \mathsf{ViralHepatitis} \wedge \mathsf{ViralHepatitis} \sqsubseteq \mathsf{Hepatitis}\)

\( \rightarrow \mathsf{ViralHepatitisB} \sqsubseteq \mathsf{Hepatitis}\)

Case-2: Modals on LHS, No Modals on RHS. The following original rule (rdfs3) from [7] imposes a range restriction on objects of binary ABox relation instances: \(\mathsf{\forall P.C \wedge P(x, y) \rightarrow C(y)}\). The extended version needs to address the ABox proposition in the antecedent (don’t care modal \(\delta \)), but must not change the consequent (even though we always use the \(\top \) modality here—the range restriction C(y) is always true, independent of the uncertainty of P(x, y); cf. Sect. 2 example):

$$ \mathsf{(Mrdfs3)} \mathsf{\forall P.C \wedge \delta P(x, y) \rightarrow \top C(y) } $$

Example rule instantiation:

\( \forall \mathsf{suffersFrom.Disease} \wedge L \mathsf{suffersFrom}(x, y) \rightarrow \top \mathsf{Disease}(y)\)

Case-3: Keeping LHS Modals on RHS. Inverse properties switch their arguments [18] as described by (rdfp8): \(\mathsf{P \equiv Q^- \wedge \mathsf P(x, y) \rightarrow Q(y, x)}\). The extended version simply keeps the modal operator:

$$ \mathsf{(Mrdfp8)} \mathsf{P \equiv Q^- \wedge \delta P(x, y) \rightarrow \delta Q(y, x) } $$

Example rule instantiation:

\( \mathsf{containedIn} \equiv \mathsf{contains}^- \wedge C \mathsf{containedIn}(x, y) \rightarrow C \mathsf{contains}(y, x)\)

Case-4: Aggregating LHS Modals on RHS. Now comes the most interesting case of modalized RDFS & OWL entailment rules, that offers several possibilities on a varying scale between skeptical and credulous entailments, depending on the degree of uncertainty, as expressed by the measuring function \(\mu \) of the modal operator. Consider the original rule (rdfp4) from [18] for transitive properties:  \(\mathsf{P^+ \sqsubseteq P \wedge P(x, y) \wedge P(y, z) \rightarrow }\) P(xz).

Now, how does the modal on the RHS of the extended rule look like, depending on the two LHS modals? There are several possibilities. By operating directly on the modal hierarchy, we are allowed to talk about, e.g., the least upper bound or the greatest lower bound of \(\delta _1\) and \(\delta _2\). When taking the associated confidence intervals into account, we might play with the low and high numbers of the intervals, say, by applying min/max, the arithmetic mean or even by multiplying the corresponding numbers. Let us first consider the general rule from which more specialized versions can be derived, simply by instantiating the combination operator \(\odot \):

$$ \mathsf{(Mrdfp4)} \mathsf{P}^+ \sqsubseteq \mathsf{P} \wedge \delta _1 \mathsf{P(x, y)} \wedge \delta _2 \mathsf{P(y, z)} \rightarrow (\delta _1 \odot \delta _2) \mathsf{P(x, z)} $$

Here is an instantiation of (Mrdfp4) as used in HFC, dealing with the transitive relation contains from above, assuming that \(\odot \) reduces to the least upper bound (i.e., \(C \odot L = L\)):

\( C \mathsf{contains}(x, y) \wedge L \mathsf{contains}(y, z) \rightarrow L \mathsf{contains}(x, z)\)

What is the general result of \(\delta _1 \odot \delta _2\)? It depends, probably both on the application domain and the epistemic commitment one is willing to accept about the “meaning” of gradation words/modal operators. To enforce that \(\odot \) is at least both commutative and associative (as is the least upper bound) is probably a good idea, making the sequence of modal clauses order independent. And to work on the modal hierarchy instead of combining low/high numbers of the corresponding intervals is probably a good decision for forward chaining engines, as the latter strategy might introduce new individuals through operations such as multiplication, thus posing a problem for the implementation of the generalization schema (G) (see Sect. 5.1).

6 Adding Time

Temporal databases [17] distinguish between (at least) two different notions of time and the representation of temporal change: valid time, the temporal interval in which a statement about the world is valid, and transaction time, the temporal duration during which a statement has been stored in a database (or ontology, in our case). Valid time is able to add information about the past, present, and future, given a moment in time, whereas transaction time add present time (= now) when a statement is entered to the database. At the end of this section, we will have established a transaction time extension for the modal fragment of OWL derived so far, including a set of entailment rules and a corresponding extended model theory.

6.1 Metric Linear Time

In the following, we assume that the temporal measuring system is based on a one-dimensional metric linear time \(\langle \mathcal{T}, \le \rangle \), so that we can compare starting/ending points, using operators, such as \(\le \), or pick out input arguments in aggregates, using min or max. We require, for reasons which will become clear, that time is discrete and represented by natural or rational numbers.

The implementation of HFC employs 8-byte long integers (XSD datatype long) to encode milli or even nano seconds w.r.t. a fixed starting point (Unix Epoch time, starting with 1 January 1970, 00:00:00). Alternatively, the XSD dateTime format can be used which provides an arbitrarily fine precision, if needed.

As a consequence, given a time point \(t \in \mathcal{T}\), the next smallest or successor time point would then be \(t+1\) (after a potential normalization). We often use this kind of notation to derive the ending time of a valid proposition \(\top \phi @ t\) from the time it gets invalidated: \(\bot \phi \)@t+1; see Sect. 6.3.

6.2 Valid Time

Valid time is a useful concept when representing, e.g., biographical knowledge which has been obtained from the Web. Various forms of OWL representations involving time have been investigated [6, 13, 19]. However, reasoning and querying with such representations is extremely complex, expensive, and error-prone and standard OWL reasoning is no longer applicable. In [10], we have investigated valid time for a non-graded extension of RDFS and OWL (triples, binary relation instances), representing the time period of an atemporal statement by two further argument, giving us quintuples instead of triples in the end. This extension is a pure syntactic calculus, defined as a set of tableaux-like entailment rules à la [7, 18], able to derive useful new information in a temporal environment. For instance, the standard entailment rule (rdfp4) in OWL for transitive properties (see Sect. 5.3)

$$\begin{aligned} \mathsf{P^+ \sqsubseteq P \wedge P(x, y) \wedge P(y, z) \rightarrow P(x, z)} \end{aligned}$$

then becomes

$$ \mathsf{P^+ \sqsubseteq P} \wedge \mathsf{P(x, y}, b_1, e_1) \wedge \mathsf{P(y, z}, b_2, e_2) \wedge [b_1, e_1] \cap [b_2, e_2] \ne \emptyset \rightarrow \mathsf{P(x, z}, b, e) $$

where \([b_1, e_1]\) and \([b_2, e_2]\) are the temporal intervals during which P(x,y) and P(y,z) are valid, given \(b = { max}(b_1, b_2)\) and \(e = { min} (e_1, e_2)\). I.e., P(x,z) is only valid during the proper intersection of \([b_1, e_1]\) and \([b_2, e_2]\). This is depicted in the following figure:

$$ \begin{array}{l} \mathop {\shortmid \text{--------------- }\shortmid }\limits ^{\mathsf{P(y, z)}} \\ \mathop {\shortmid \text{--------- }\shortmid }\limits ^{\mathsf{P(x, y)}} \\ \cdots \text{--------- }_{b_1}\!\!\!\text{--- }_{b_2}\!\!\!\text{----- }_{e_1}\!\!\!\!\!\text{----------- }_{e_2}\!\!\!\!\!\text{------------------ }\triangleright t \end{array} $$

Note that P(x,z) is definitely the case for [be], but we do not know if it holds before b or after e. This inference harmonizes well with the open-world assumption underlying OWL.

In HFC, the meaning of the original entailment rule (left) and the extension for valid time (right) can be straightforwardly derived from the abstract syntax above:

figure g

In HFC, IntersectionNotEmpty refers to the (Java) implementation of a specific method of the corresponding class which realizes the above intersection of the corresponding temporal intervals (pseudo code):

figure h

This computationally cheap left-hand side test (cf. the @test section in the above HFC rule) is applied after LHS matching and before right-hand side instantiation. The RHS generation of the resulting interval [be] is achieved by the two aggregates Max and Min whose return values are bound to the RHS-only rule variables ?b and ?e, resp. (cf. the @action section above). It is worth noting that these two aggregates do not generate brand-new individuals (contrary to addition, for example), thus a terminating rule set and so a finite model is guaranteed overall.

The interesting observation when adding valid time to the RDFS & ter Horst subset of OWL is that only an additional test (cf. IntersectionNotEmpty) and two aggregates (cf. Max, Min) are needed [10]. Almost the same is true when adding transaction time to the modal extension of RDFS & OWL that we have investigated so far in the first part of this article. The additional test in HFC is called ValidInBetween and the aggregates are Min and Max, as before.

6.3 Transaction Time

Like valid time, the original approach to transaction time makes use of temporal intervals in order to represent the time during which a fact is stored in the database, even though the ending time is not known in advance. This is indicated by the wildcard ? which will later be overwritten by the concrete ending time.

We deviate here from the interval view by specifying both the starting time when an ABox statement is entered to an ontology, and, via a separate statement, the ending time when the statement is invalidated.Footnote 4 For this, we exploit the propositional modals \(\top \) and \(\bot \) from before. This idea is shown in the following figure for a binary relation P. We write P(c,d,b,e) to denote the row in the database table P for relation P.

figure i

As we see from this picture, the invalidation in the ontology happens at \(t_2\)+1, whereas \([\mathtt{t_1,t_2}]\) specifies the transaction time in the database. Clearly, the same transaction time interval for P(c,d) in the ontology can be derived from the two statements \(\top \mathsf{P(c,d)@}{t_1}\) and \(\bot \mathsf{P(c,d)@}{t_2+1}\), assuming that there does not exist a \(\bot \mathsf{P(c,d)@}{t}\), such that \(t_1 \le t \le t_2\) (we can effectively query for this by employing the ValidInBetween test).

Extending ontologies by transaction time the way we proceed here gives us a means to easily encode time series data, i.e., allows us to record the history of data that changes over time, and so simulating imperative variables in a declarative environment.

6.4 Entailment Rules for Graded Modals and Transaction Time

We have almost introduced the abstract syntax for graded propositions with transaction time (\(\delta \in \triangle \))

$$\begin{aligned} \delta \phi @ t \end{aligned}$$

Here, we focus on the binary relation case in order to address the RDFS [7] and ter Horst extension of OWL [18] from above. For this, we will then write

$$\begin{aligned} \delta \mathsf{P(c,d)} @ t \end{aligned}$$

The corresponding quintuple representation in HFC then becomes

figure j

We opt for a uniform representation, thus axiomatic triples need to be extended by two further arguments; for instance,

becomes

figure k

We read the above statement as being true (\(\top \) = logic:true) from the beginning of time (long int 0 = ). We are now ready to distinguish, again, between the four principled cases from Sect. 5.3, where we compared the original rules from [7, 18] to the graded modal extension, but now extend them further by a transaction time argument.

Case-1: Top Modals Only, Zero Time. We have already seen that the entailment rule (rdfs11) from [7] deals with class subsumption: \(\mathsf{C \sqsubseteq D \wedge D \sqsubseteq E \rightarrow C \sqsubseteq E}\). As this rule concerns only terminological knowledge (TBox), we decided not to change it in the modal domain. Since we argued above for a uniform quaternary relation or quintuple representation, this rule leads us quite naturally to the extended version of (rdfs11):

figure l

This notation simply highlights that the original class subsumption entailment is true at every time, i.e., expresses an universal truth (remember the meaning of \(\top \) and transaction time 0, and compare this to the axiomatic triple from above).

Case-2: Modals on LHS, Top Modals on RHS, Keeping Time. The original rule (rdfs3) from [7] imposes a range restriction on P: \(\mathsf{\forall P.C \wedge P(x, y) \rightarrow C(y)}\). Adding modals gave us (Mrdfs3): \(\mathsf{\forall P.C \wedge \delta P(x, y) \rightarrow \top C(y) }\). Extending this rule with transaction time is easy:

figure m

The range restriction is a universal RBox statement (thus \(\top \) and 0). P(x,y) is graded (\(\delta \)) and happens at a specific time t. Thus, the class prediction C(y) of the range argument y at time t is true (\(\top \)).

Case-3: Keeping LHS Modals on RHS, Keeping Time. Inverse properties are described in [18] by (rdfp8): \(\mathsf{P \equiv Q^- \wedge \mathsf P(x, y) \rightarrow Q(y, x)}\). The modalized version simply kept the modal operator (Mrdfp8): \(\mathsf{P \equiv Q^- \wedge \delta P(x, y) \rightarrow \delta Q(y, x) }\). The transaction time version furthermore takes over the temporal argument:

figure n

Again, \(\mathsf{P \equiv Q^-}\) is a universal RBox statement (use \(\top \) and0) and both the grading of \(\mathsf{P(x, y)}\) and time t is consequently transferred to \(\mathsf{Q(y, x)}\).

Case-4: Aggregating Modals, Aggregating Time. This case is the most challenging and computationally expensive one. The concrete implementation in HFC employs the above-mentioned test ValidInBetween (two times use in lines 2 and 3 below in a different form) and the aggregates Min and Max. Again, we will focus on one specific rule here, viz., (rdfp4) from [18] for transitive properties: \(\mathsf{P^+ \sqsubseteq P \wedge P(x, y) \wedge P(y, z)\rightarrow }\) P(xz). The modal extension led us to (Mrdfp4): \(\mathsf{P}^+ \sqsubseteq \mathsf{P} \wedge \delta _1 \mathsf{P(x, y)} \wedge \delta _2 \mathsf{P(y, z)} \rightarrow (\delta _1 \odot \delta _2) \mathsf{P(x, z)}\). This blueprint can be utilized to derive the final transaction time version:

figure o

Lines 1 and 4 of (TMrdfp4) are easy to grasp when compared to the plain modal extension (Mrdfp4) and the fact that the transaction time for the consequent \((\delta _1 \odot \delta _2)\) P(x,z) is based on the time when both \(\delta _1\) P(x,y) and \(\delta _2\) P(y,z) are the case, i.e., \({ max}(t_1, t_2)\):

figure p

Furthermore, lines 2 and 3 guarantee that graded contradictory information with an equal or less degree of uncertainty \(||\delta _{1,2}^\mathsf{M}||\) (i.e., equal or more trustworthiness) does not exist as it would argue too strongly against the graded entailment of P(x, z). Here, it is important to understand the interplay between (TMrdfp4) and the extension of the binary generalization schema (G) from Sect. 5.1:

figure q

Consider, for example, that \(\delta _1 \mathsf{P(x,y)} @ t_1\) matches \(C \mathsf{P(x,y)} @ 30\) and \(\delta _2 \mathsf{P(y,z)} @ t_2\) matches \(L \mathsf{P(y,z)} @ 42\) in (TMrdfp4). Given statement \(E \mathsf{P(x,y)} @ 40\) (\(30 \le 40 \le 42\)), we are thus not allowed to derive the instantiation of the antecedent of (TMrdfp4). The more certain statement \(\bot \mathsf{P(x,y)} @ 40\) does also not support the rule as (TG) would allow us to derive \(E \mathsf{P(x,y)} @ 40\) again. Only a more uncertain modal than E will do the trick, e.g., U (recall that \(||\bot ||< ||E|| < ||U||\)). Thus, \(U \mathsf{P(x,y)} @ 40\) is a necessary requirement for finally deriving \((C \odot L) \mathsf{P(x,z)} @ 42\).

6.5 Model Theory for Graded Modals and Transaction Time

The model theory for graded modals including transaction time will not differ much from what we already introduced in Sects. 4.2 and 4.3. Time points \(t \in \mathcal{T}\), indicated by the notation @t relative to a proposition P(x,y), are related to what hybrid logics [3] call nominalshandles to worlds which are indexed by t and which are made available in the syntax of the modal language via @t. In our setting and contrary to hybrid logics, t does not refer to a single world, but to multiple ones.

For transaction time, we still keep the notion of a frame \(\mathcal{F} = \langle \mathcal{W}, \mathcal{R}_\triangle , \preceq \rangle \) and, in principle, that of a model \(\mathcal{M} = \langle \mathcal{F}, \mathcal{V}, \mu \rangle \) (see Sect. 4.2). However, we will modify the valuation function \(\mathcal{V}: \Phi \mapsto 2^\mathcal{W}\) in that its domain now also takes time points from \(\mathcal{T}\) into account; i.e., \(\mathcal{V}: \Phi \times \mathcal{T} \mapsto 2^\mathcal{W}\) returns those worlds at which \(\phi @ t\) is valid, given \(\phi \in \Phi \) and \(t \in \mathcal{T}\). This directly leads us to the extension of the six cases for the satisfaction relation \(\models \) from Sects. 4.2 and 4.3:

  1. 1.

    \(\mathcal{M}, w \models p(\mathbf {c}) @ t\)  iff  \(w \in \mathcal{V}(p(\mathbf {c}), t)\) and \(w \not \in \mathcal{V}(\lnot p(\mathbf {c}), t)\)

  2. 2.

    \(\mathcal{M}, w \models \lnot p(\mathbf {c}) @ t\)  iff  \(w \in \mathcal{V}(\lnot p(\mathbf {c}), t)\) and \(w \not \in \mathcal{V}(p(\mathbf {c}), t)\)

  3. 3.

    \(\mathcal{M}, w \models \phi @ t \wedge \phi ^\prime @ t^\prime \)  iff  \(\mathcal{M}, w \models \phi @ t\) and \(\mathcal{M}, w \models \phi ^\prime @ t^\prime \)

  4. 4.

    \(\mathcal{M}, w \models \phi @ t \vee \phi ^\prime @ t^\prime \)  iff  \(\mathcal{M}, w \models \phi @ t\) or \(\mathcal{M}, w \models \phi ^\prime @ t^\prime \)

  5. 5.

    for all \(\delta \in \underline{1}\): \(\mathcal{M}, w \models \delta \pi @ t\) iff  \(\frac{\#\,\cup _{\delta ^\uparrow \succeq \delta }\{u \mid (w, u) \in R_{\delta ^\uparrow } \;{ \mathbf{and}}\; \mathcal{M}, u \models \pi @ t\}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

  6. 6.

    for all \(\delta \in \underline{0}\): \(\mathcal{M}, w \models \delta \pi @ t\) iff  \(1 - \frac{\#\,\cup _{\delta ^\uparrow \succeq \delta }\{u \mid (w, u) \in R_{\delta ^\uparrow } \;{ \mathbf{and}}\; \mathcal{M}, u \models \pi @ t\}}{\#\,\cup _{\delta ^\prime \in \triangle }\{v \mid (w, v) \in R_{\delta ^\prime }\}} \in \mu (\delta )\)

We also keep constraint \((\mathcal{C}_1)\) for well-behaved frames, but need to modify constraint \((\mathcal{C}_2)\) to incorporate transaction time (cf. Sect. 4.3):

$$ \begin{array}{ll} (\mathcal{C}_2) &{} \mathbf{if} \; (w, u) \in R_\delta \; \mathbf{s.t.} \; u \in \mathcal{V}(\lnot \phi , t) \\ &{} \mathbf{then} \; \exists u^\prime \in \mathcal{W} \; \mathbf{s.t.} \; (w, u^\prime ) \in R_{\delta ^\mathsf{M}} \; \mathbf{and} \; u^\prime \in \mathcal{V}(\phi , t) \end{array} $$

Furthermore, we impose a third constraint on the relational structure \(\mathcal{F}\) which models the intuition if \(\phi \) is valid at time t, so is \(\phi \) at \(t+1\), in case nothing argues heavily against \(\phi \) (compare this to a similar argumentation expressed by lines 2 and 3 in (TMrdfp4) of case 4 in Sect. 6.4):

$$ \begin{array}{ll} (\mathcal{C}_3) &{} \mathbf{if} \; (w, u) \in R_\delta \; \mathbf{s.t.} \; u \in \mathcal{V}(\phi , t) \; \mathbf{and} \; \not \exists (w, v) \in R_{\delta ^\mathsf{M}} \; \mathbf{s.t.} \; v \in \mathcal{V}(\phi , t) \\ &{} \mathbf{then} \; \exists (w, x) \in R_\delta \; \mathbf{s.t.} \; x \in \mathcal{V}(\phi , t + 1) \end{array} $$

Here, however, we do not need to check for proposition \(\delta ^\mathsf{M} \phi \) between t and \(t+1\), as time is discrete and normalized, so that \(t+1\) is the immediate successor of t.

Constraint \((\mathcal{C}_3)\) can be seen as a kind of forward monotonicity in that valid propositions at time t will always hold at time \(t+1\). As a consequence, this will give us an infinite frame (cf. the existential variable x in the consequent), i.e., an infinite number of worlds. To implement such a kind of model behaviour in the syntax through a finite number of propositions, we make the following assumption. Propositions will never be brought to the temporal forefront (never being updated), i.e., there is no rule such as \(\delta \phi @ t \rightarrow \delta \phi @ (t+1)\). Only if \(\delta \phi \) needs to be invalidated at \(t^\prime \), we will add the further statement \(\bot \phi @ t^\prime \). Thus, through the use of the test ValidInBetween from above, we are then able to query whether \(\delta \phi \) is still valid at a different time \(t^{\prime \prime } > t\).

7 Summary

In this paper, we have explored a fragment of a non-standard modal logic, being able to represent graded statements about the world. The modal operators in the syntax of the modal language were derived from gradation words and were further extended through mirror and complement operations. The operators were interpreted through confidence intervals in the model theory for expressing the uncertainty about the validity of a proposition. The model theory was complemented by a set of RDFS-/OWL-like entailment rules, acting on the syntactic representation of modalized statements. Finally, we extended the framework by transaction time in order to implement a notion of temporal change. The framework has been implemented in HFC for the case of binary propositions.