Abstract
The subject matter of this thesis is twofold. On the one hand, this work investigates first-order temporal logic on finite temporal, called finite traces, focussing on the comparison with the usual infinite trace semantics and on the computational complexity of decidable fragments, which also constitute the backbone of temporal description logics. On the other hand, we explore the addition of constructors for definite descriptions, i.e., possibly non-denoting expressions of the form ‘the x suchthat ϕ’, to description logic formalisms. To follow these parallel (and yet connected) research directions, after a shared Prologue, the thesis branches into two parts.
In Part I, on first-order temporal logic on finite traces, we introduce the syntax of this language and its semantics, based either on the natural numbers, or on finite initial segments thereof. We then investigate the relationships between finite and infinite traces semantics, focussing on satisfiability and equivalences of
formulas, and provide sufficient conditions to guarantee when the distinction between reasoning over finite and infinite traces can be safely blurred. In addition, we study the computational complexity of satisfiability on finite traces for several decidable fragments of first-order temporal logic, including temporal description logics. Finally, we establish connections with planning and runtime verification notions.
In Part II, we investigate free description logics with definite descriptions, where both individual names and definite descriptions are included as terms of the language, and the semantics accounts for their possible lack of denotation. We extend with such features two well-known description logics equipped with nominals and the universal role, showing that standard reasoning in these extensions is not harder than in the original languages. We then characterise the expressive power of concepts relative to first-order formulas using a suitable notion of bisimulation. Moreover, we study the complexity of deciding the existence of definite descriptions for an individual under an ontology. Finally, we provide a polynomial-time reduction of reasoning in other free description logics based on dual-domain semantics to our setting.
In the Epilogue of this work, we start connecting Part I and II of the thesis. We present temporal free description logics with definite descriptions, extending the usual temporal description logics with definite descriptions, and additionally assuming that individual names and definite descriptions are interpreted non-rigidly, meaning that the object they denote can change over time. A preliminary negative result, concerning the undecidability of satisfiability on finite traces for a temporal description logic with the universal role and non-rigid nominals, is provided.