Reasoning with Temporal ABoxes: Combining DL-Lite_core with CTL.
Francesco Pagliarecci, Luca Spalazzi, Gilberto Taccari · Università Politecnica delle Marche (Università Politecnica delle Marche) · 2013
Abstract. The work shows the combination of standard description logics (DLs) with standard temporal logics (TLs). Indeed, the introduction of DLs as logic-based knowledge representation formalisms has emerged in many fields and many applications have taken advantage from it. Although that, in many of these applications also temporal aspects play an important role. It follows that a new formalism is needed in order to represent both terminological and temporal knowledge. At this aim, the majority of research works proposed the combination of DLs and TLs producing a new formalism to knowledge representation: temporal description logics (TDLs). This work illustrates the combination of the dl-litecore description logic with the temporal logic ctl. It defines a temporal knowledge base with time-invariant tbox and time-variant abox. Furthermore an algorithm based on semantic model checking is proposed in order to query the knowledge base.