Software Model Checking is emerging as one of the leading approaches to automatic program analysis. State-of-the-art software model checkers exhibit levels of automation and precision often superior to those provided by traditional software analysis tools. This success is due to a large extent to the use of Satisfiability Modulo Theory (SMT) solvers to support reasoning about complex and even infinite data structures (e.g. bit-vectors, numeric data, arrays) manipulated by the program being analysed. In this talk I will survey the opportunities and challenges posed to Automated Reasoning by this new application domain.

We review and extend earlier work on the logic ${\cal CFD}$, a description logic with universal restrictions over functional roles and that allows terminological cycles. In particular, we consider the problem of reasoning about concept subsumption and the problem of computing certain answers for a family of attribute-connected conjunctive queries, showing that both problems are in PTIME. We then consider the effect on the complexity of these problems after adding a concept constructor that expresses concept union, or after adding a concept constructor for the bottom class. Finally, we show that adding both constructors makes both problems EXPTIME-complete.

In our previous work we have developed a method for completing a Description Logic knowledge base w.r.t. a fixed interpretation by asking questions to a domain expert. Our experiments showed that during this process the domain expert sometimes gives wrong answers to the questions, which cause the resultant knowledge base to have unwanted consequences. In the present work we consider the problem of explaining the reasons of such unwanted consequences in knowledge base completion. We show that in this setting the problem of deciding the existence of an explanation within a specified cardinality bound is NP-complete, and the problem of counting explanations that are minimal w.r.t. set inclusion is #P-complete. We also provide an algorithm that computes one minimal explanation by performing at most polynomially many subsumption tests.

We present a fragment of multi-sorted set-theoretic formulae, called $3LQS$, that admits a restricted form of quantification over individual and set variables, and show that it has a solvable satisfiability problem. The proof is carried out by showing that the theory $3LQS$ enjoys a small model property, i.e., any satisfiable $3LQS$-formula $\psi$ has a finite model whose size depends solely on the size of $\psi$ itself.

Description logics (DLs) are successfully used in a variety of applications. In particular, this includes the use of DLs as an ontology language and for reasoning about conceptual database models such as ER diagrams and UML class diagrams. In many of these applications, there is a need to extend DLs with a temporal component. Notably, medical ontologies such as \mbox{SNOMED CT} often comprise concepts whose faithful modelling requires to capture also temporal aspects. An example is SNOMED CT's concept ``concussion without loss of consciousness'', which describes a concussion after which the patient has remained conscious until the time of examination. Temporal expressivity is also required when the DL approach to reasoning about conceptual database models is lifted from traditional databases to temporal ones. These observations have led to an extensive and varied literture on temporal DLs (TDLs).

In this talk, I will survey a family of TDLs that is obtained by combining DLs with temporal logics such as LTL and CTL. I will start with the basic members of this family, which allow the application of temporal operators to DL concepts, only. In this basic case, the interaction between the temporal component and the DL component of the TDL is limited, and very transparent decision procedures can be obtained. I will then discuss more powerful combinations that are obtained by allowing the application of temporal operators also to TBox statements and roles. In the former case, reasoning is still decidable, but decision procedure are more involved (and interesting). In the latter case, reasoning is undecidable and I will discuss a number of ways that have been proposed to circumnavigate this problem. Finally, I will put temporal DLs into the perspective of so-called monodic fragments of temporal first-order logic.

Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate this set incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and may terminate on both satisfiable and unsatisfiable input without generating the whole set of instances needed in standard local reasoning.

In this paper we present our work in progress towards obtaining a Nelson-Oppen style combination for combining quantified theories, where each individual component theory admits quantifier elimination. We introduces the notion of good models for union theories, and show that for the good models of union theories, there exists a simple quantifier elimination scheme which uses the elimination procedures for individual component theories as black boxes. Using a priority argument, we show that good models exist for the union theory of dense linear order and random graph.