Temporalising Tractable Description Logics

It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of 'weak' description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable.

Authors

• Alessandro Artale
• Roman Kontchakov
• Carsten Lutz
• Frank Wolter
• Michael Zakharyaschev

Keywords

• Automatic logic units
• Ontologies
• Computer science
• Educational institutions
• Computational complexity
• History
• Logic design
• Biomedical informatics
• Description Logic
• Binary Relation
• Temporal Logic
• Semantic
• Number Of Types
• Conceptual Model
• Temporal Model
• Local Names
• Object Naming
• Temporal Constraints
• First-order Logic
• Form Of Formula
• Set Of Names
• Suitable Pair
• Temporal Operators