Temporal description logics formally represent, and enable reasoning about, time-dependent concepts, actions, and video events. The main approaches to employ standard temporal logic operators, such as the unary operators ○ (at the next state), ⋄ (eventually), and □ (globally), and the binary operator U (until), with general-purpose description logics aimed at representing terminological knowledge of a domain include the following:
- Add temporal operators as additional concept constructors
- Apply the temporal operators to the TBox, the ABox, and roles
- Combine the above two
Such combinations are based on two-dimensional semantics, where one dimension represents time using point-based or interval-based temporal logic and the other the knowledge domain using a standard description logic. Logics combined with conventional description logics to form temporal description logics include, but are not limited to, the time interval logic of Halpern and Shoham, Prior’s tomorrow tense logic, and standard temporal logics (TL), such as LTL (Linear Time Temporal Logic) and CTL (Computational Tree Logic). Some temporal description logics utilize the formal representation of video events, others employ time point and time interval datatype definitions.
The basic temporal description logic TL-F is composed of the temporal language TL, which expresses interval temporal networks, and the non-temporal Feature Description Logic F. More expressive temporal description logics include TLU–FU, which adds disjunction to both the temporal and the non-temporal sides of TL-F, and TL-ALCF, which extends the non-temporal side of TL-F with roles and full propositional calculus.
CIQU is an extension of CIQ with the binary temporal operator U (until), which may be applied to concepts and formulae. CIQUS is an extension of CIQ with the binary temporal operators U (until) and S (since), both of which may be applied to concepts and formulae.DLRUS is a temporal description logic similar to TL-ALCF, although provides a point-based rather than an interval-based temporal structure. It is the extension of the DLR description logic with the temporal operators Until and Since.
TL-SI consists of the temporal logic TL and the description logic SI.
Temporal Extensions of ALC
T-ALC is the temporal extension of the core description logic ALC with time intervals. TL-ALC is another temporal extension of ALC, which features the temporal operators ○ (next) and U (until) applied to concepts and formulae. The temporal description logic TL-ALCF is composed of the interval-based temporal logic TL and the non-temporal description logic ALCF, and was designed for domains with objects which have properties that vary over time. Further ALC-based temporal description logics include ALC-LTL and the combination and modification of the description logic ALC and Prior’s tomorrow tense logic, XALC, and BALCl.