Definite descriptions are expressions of the form „the unique x satisfying property C,” which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an alternative to proper names (IDs), which lack semantic content and serve merely as placeholders. In this paper, we introduce two extensions of the well-known description logic ALC with local and global definite descriptions, denoted ALCiL and ALCiG, respectively. We define appropriate bisimulation notions for these logics, enabling an analysis of their expressiveness. We show that although both logics share the same tight ExpTime complexity bounds for concept and ontology satisfiability, ALCiG is strictly more expressive than ALCiL. Moreover, we present tableau-based decision procedures for satisfiability in both logics, provide their implementation, and report on a series of experiments. The empirical results demonstrate the practical utility of the implementation and reveal interesting correlations between performance and structural properties of the input formulas.

DatalogMTL is a powerful extension of Datalog with operators from metric temporal logic (MTL), which has received significant attention in recent years. In this paper, we investigate materialisation-based reasoning (a.k.a. forward chaining) in the context of DatalogMTL programs and datasets with bounded intervals, where partial representations of the canonical model are obtained through successive rounds of rule applications. Although materialisation does not naturally terminate in this setting, it is known that the structure of canonical models is ultimately periodic. Our first contribution in this paper is a detailed analysis of the periodic structure of canonical models; in particular, we formulate saturation conditions whose satisfaction by a partial materialisation implies an ability to recover the full canonical model via unfolding; this allows us to compute the actual periods describing the repeating parts of the canonical model as well as to establish concrete bounds on the number of rounds of rule applications required to achieve saturation. Based on these theoretical results, we propose a practical reasoning algorithm where saturation can be efficiently detected as materialisation progresses, and where the relevant periods used to evaluate entailment of queries via unfolding are efficiently computed. We have implemented our algorithm and our experiments suggest that our approach is both scalable and robust.

We study the problem of efficiently computing all (usually infinitely many) facts which are entailed by a specification written in linear temporal logic (LTL)-a standard formalism for specifying and verifying properties of computations in reactive systems. This problem can be seen as a generalisation of the standard entailment checking, but whose output provides a much wider understanding of the system’s behaviour. We show that in full LTL the problem can be solved in doubly exponential time, whereas for Horn fragments of LTL, which can be seen as temporal logic programs, the problem can be solved in exponential or only quadratic time, depending on the allowed temporal operators in the input formula. Moreover, we show that all these bounds are optimal. We also implement and experimentally compare two techniques for solving the problem: an automata-based algorithm for full LTL and a materialisation-based algorithm for Horn fragments. The obtained results suggest practical usefulness of our approach.

DatalogMTL is an extension of Datalog with metric temporal operators that has recently found applications in stream reasoning and temporal ontology-based data access. In contrast to plain Datalog, where materialisation (a.k.a. forward chaining) naturally terminates in finitely many steps, reaching a fixpoint in DatalogMTL may require infinitely many rounds of rule applications. As a result, existing reasoning systems resort to other approaches, such as constructing large Büchi automata, whose implementations turn out to be highly inefficient in practice. In this paper, we propose and study finitely materialisable DatalogMTL programs, for which forward chaining reasoning is guaranteed to terminate. We consider a data-dependent notion of finite materialisability of a program, where termination is guaranteed for a given dataset, as well as a data-independent notion, where termination is guaranteed regardless of the dataset. We show that, for bounded programs (a natural DatalogMTL fragment for which reasoning is as hard as in the full language), checking data-dependent finite materialisability is ExpSpace-complete in combined complexity and PSpace-complete in data complexity; furthermore, we propose a practical materialisation-based decision procedure that works in doubly exponential time. We show that checking data-independent finite materialisability for bounded progams is computationally easier, namely ExpTime-complete; moreover, we propose sufficient conditions for data-indenpendent finite materialisability that can be efficiently checked. We provide also the complexity landscape of fact entailment for different classes of finitely materialisable programs; surprisingly, we could identify a large class of finitely materialisable programs, called MTL-acyclic programs, for which fact entailment has exactly the same data and combined complexity as in plain Datalog, which makes this fragment especially well suited for big-scale applications.

Abstract Sentential Calculus with Identity ( $$\mathsf {SCI}$$ SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $$\mathsf {SCI}$$ SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of $$\mathsf {SCI}$$ SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for $$\mathsf {SCI}$$ SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for $$\mathsf {SCI}$$ SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

DatalogMTL is an extension of Datalog with metric temporal operators that has recently received significant attention. In contrast to plain Datalog, where scalable implementations are often based on materialisation (a.k.a. forward chaining), reasoning algorithms for recursive fragments of DatalogMTL are automata-based and not well suited for practice. In this paper we propose the class of finitely materialisable DatalogMTL programs, for which forward chaining reasoning terminates after finitely many rounds of rule application. We show that, for bounded programs (a large fragment of DatalogMTL where temporal intervals are restricted to not mention infinity), checking whether a program is finitely materialisable is feasible in exponential time, and propose sufficient conditions for finite materialisability that can be checked more efficiently. We finally show that fact entailment over finitely materialisable bounded programs is ExpTime-complete, and hence no harder than Datalog reasoning.

We present a modal logic for representing and reasoning about space seen from the subject’s perspective. The language of our logic comprises modal operators for the relations "in front", "behind", "to the left", and "to the right" of the subject, which introduce the intrinsic frame of reference; and operators for "behind an object", "between the subject and an object", "to the left of an object", and "to the right of an object", employing the relative frame of reference. The language allows us to express nominals, hybrid operators, and a restricted form of distance operators which, as we demonstrate by example, makes the logic interesting for potential applications. We prove that the satisfiability problem in the logic is decidable and in particular PSpace-complete.

In this paper, we present a program designed to successfully and autonomously play Angry Birds, which attempts to embrace motives of human players in their choices of targets they want to shoot at in a game play. The program comprises two modules: the representation module and the reasoning module. In the former, we introduce qualitative space representation that utilizes notions such as “to lie on,” “to lie to the right,” “to be a shelter of a target,” etc. The latter investigates how particular blocks of a structure behave once one of them has been hit. It includes two algorithms, namely vertical impact and horizontal impact. The first one is a novel method of investigating the behavior of complex structures after one of their constituent blocks gets hit. Namely, it predicts which elements of a structure fall if a supporting block gets destroyed. Horizontal impact, on the other hand, simulates force propagation between adjacent elements after one of them gets struck. We also describe experimental tests we have conducted in which Vertical Impact correctly predicted which blocks will fall in over 98% of investigated cases.