ABSTRACT. This talk will discuss a very general notion of query reformulation: Given a query Q, a set of constraints Sigma, a target query language or programming language, and a cost metric, determine if there is an object in the target language that is equivalent to Q relative to the constraints, and if so find such an object optimizing the cost metric.

The problem has a long history in the database community, originally motivated by querying over materialized views. This talk will go over several very-recent developments—from a database perspective, but mentioning the relationship to description logics.

We will first go over the connection between reformulation and interpolation/preservation properties, originating in the work of Nash, Segoufin, and Vianu, and show how this can be extended to give a very elegant theoretical framework for studying the reformulation problem. After that we will turn to performing interpolation and reformulation directly over a physical plan language, rather than a query language. This will include a discussion of:

-- how to extend traditional cost-based query optimization to the setting of constraint-based reformulation

-- how to "plug in" reasoners, particularly those for expressive decidable logics (guarded negation, guarded TGDs), into the reformulation process.

This includes work with Balder ten Cate, Julien Leblay, Efi Tsamoura, and Michael Vanden Boom.

ABSTRACT. The complete picture of the complexity of conjunctive query answering under guarded disjunctive existential rules has been recently settled. However, in the case of acyclic (unions of) conjunctive queries there are some fundamental questions which are still open. It is the precise aim of the present paper to close those questions. Our main result states that acyclic conjunctive query answering under a fixed set of guarded disjunctive existential rules is EXPTIME-hard. This result together with an EXPTIME upper bound obtained by exploiting classical results on guarded first-order logic, gives us the complete picture of the complexity of our problem. As an immediate consequence, we get that answering acyclic unions of conjunctive queries under DL-Lite_{bool}^{H}, one of the most expressive languages of the DL-Lite family of DLs, is EXPTIME-complete, even in the case of a fixed TBox. In fact, the EXPTIME-hardnees holds even for DL-Lite_{bool}, that is, the DL obtained from DL-Lite_{bool}^{H} after forbidding role hierarchies.

ABSTRACT. Nominal schemas extend description logics (DLs) with a restricted form of variables, thus integrating rule-like expressive power into standard DLs. They are also one of the most recently introduced DL features, and in spite of many works on algorithms and implementations, almost nothing was known about their computational complexity and expressivity until recently. In this extended abstract, we review our recent work "Nominal Schemas in Description Logics: Complexities Clarified" that will be presented at KR 2014. We give a comprehensive overview of the reasoning complexities of a wide range of DLs—from EL to SROIQ—extended with nominal schemas. Both combined and data complexities increase by one exponential in most cases, with the one previously known case of SROIQ being the main exception. To further improve our understanding of nominal schemas, we also investigate their semantics, traditionally based on finite grounding, and show that it can be extended to infinite sets of individuals without affecting reasoning complexities. We argue that this might be a more suitable semantics when considering entailments of axioms with nominal schemas.

ABSTRACT. We compare the expressiveness of the description logics that extend \ALCreg (a variant of PDL) with any combination of the features: inverse roles, nominals, quantified number restrictions, the universal role, the concept constructor for expressing the local reflexivity of a role. The comparison is done for the expressiveness with respect to concepts, positive concepts and TBoxes. It is based on bisimulations.

ABSTRACT. Very expressive Description Logics in the $\Logic{SH}$ family have worst case complexity ranging from \complexity{EXPTIME} to double \complexity{NEXPTIME}. In spite of this, they are very popular with modellers and serve as the foundation of the Web Ontology Language (OWL), a W3C standard. Highly optimised reasoners handle a wide range of naturally occurring ontologies with relative ease, albeit with some pathological cases. A recent optimisation trend has been \emph{modular} reasoning, that is, breaking the ontology into hopefully easier subsets with a hopefully smaller overall reasoning time (see MORe and Chainsaw for prominent examples).

However, it has been demonstrated that subsets of an OWL ontology may be harder -- even much harder -- than the whole ontology. This introduces the risk that modular approaches might have even more severe pathological cases than the normal monolithic approaches.

In this paper, we analyse a number of ontologies from the BioPortal repository in order to isolate cases where random subsets are harder than the whole. For such cases, we then examine whether the module nearest to the random subset also exhibits the pathological behaviour.

ABSTRACT. We propose a novel approach for performance prediction of OWL reasoners. It selects suitable, small ontology subsets, and then extrapolates reasoner's performance on them to the whole ontology. We investigate intercorrelation of ontology features using PCA. Finally, we discuss various error measures for performance prediction and compare our approach against an existing one using these measures.

ABSTRACT. We present a non-deterministic consequence-based procedure for the description logic ALCHI. Just like the similar style (deterministic) procedures for EL and Horn-SHIQ, our procedure explicitly derives subsumptions between concepts, but due to non-deterministic rules, not all of these subsumptions are consequences of the ontology. Instead, the consequences are only those subsumptions that can be derived regardless of the choices made in the application of the rules. This is similar to tableau-based procedures, for which an ontology is inconsistent if every expansion of the tableau eventually results in a clash. We report on a preliminary experimental evaluation of the procedure using a version of SNOMED~CT with disjunctions, which demonstrates some promising potential.

ABSTRACT. Program Analysis requires expressive logics enjoying good computational properties and capable of describing graph-structured information. In particular, logical representation of standard dynamic data structures like lists or trees requires some form of reachability assertions. However, reachability is usually not expressible in decidable logics for graphs such as guarded first-order logic (GF), and thus in Description Logics (DLs), which are mainly fragments of GF. In this work, we introduce the DL $ALCQIO_{b,Re}$ that extends the Boolean $ALCQIO$ KBs with reachability assertions and is tailored for reasoning over programs with dynamic data structures. $ALCQIO_{b,Re}$ is powerful enough to express (an unbounded number of) lists and trees, can describe complex data structures with a high degree of sharing, and also allows compositions like trees of lists or lists of trees. We show that finite model reasoning in $ALCQIO_{b,Re}$ is polynomial-time reducible to finite satisfiability of $ALCQIO$-formulae. As a consequence, we get that finite satisfiability and finite implication in $ALCQIO_{b,Re}$ are NEXPTIME-complete. Extensions of DLs with reachability have been studied previously (mainly in terms of fix-points and regular expressions), but $ALCQIO_{b,Re}$ is the first such enriched DL that remains decidable in the simultaneous presence of nominals, inverse roles and counting quantifiers.

ABSTRACT. Regular path queries (RPQs) define query patterns in terms of regular expressions and are therefore well-suited to query for paths over roles in DL. RPQs can be extended to 2-way RPQs (with converse), CRPQs (with conjunctions), or PRPQs (arbitrary positive Boolean combinations), all of which have been explored in DL research. Another natural extension of any query language is nesting, where query predicates can be defined in terms of subqueries. In this paper, we discuss several ways of introducing nesting to PRPQs, and show that they lead to increasingly expressive query languages: CN2RPQs, which were studied in the context of DLs recently; nested P2RPQs; and positive queries with transitive closure on binary predicates. The latter is one of the most expressive languages for which query answering can still be decided over DL knowledge bases. We present initial complexity results that show query answering to be non-elementary in the worst case, with an exponential increase for each level of nesting.

ABSTRACT. Ontology modelling sometimes calls for higher order entities, i.e., classes of classes, and so on. Such constructs are, however, not supported by most widely used ontology languages, such as OWL 2, which is based on the SROIQ DL. This often results in approximate modelling techniques, such as modelling classes as individuals. Some of the logical and ontological information is thus lost, or at least obscured. In this paper we show a typed higher-order variant of SROIQ. We show that it is decidable, and in fact polynomially reducible into regular SROIQ. In the latter part of the paper we then illustrate modelling scenarios in which such a language is useful.

ABSTRACT. The language Hi(DL-LiteR) is obtained from DL-LiteR by adding metamodeling features, and is equipped with a query language that is able to express higher-order queries. We investigate the problem of answering a particular class of such queries, called instance higher-order queries posed over Hi (DL-LiteR ) knowledge bases (KBs). The only existing algorithm for this problem is based on the idea of reducing the evaluation of a higher-order query Q over a Hi(DL-LiteR) KB to the evaluation of a union of first-order queries over a DL-LiteR KB, built from Q by instantiating in all possible ways all metavariables. Even though of polynomial time complexity with respect to the size of the KB, this algorithm turns out to be inefficient in practice. In this paper we present a new algorithm, called Smart Binding Planner (SBP), that compiles Q into a program, that issues a sequence of first-order conjunctive queries, where each query has the goal of providing the bindings for metavariables of the next ones, and the last one completes the process by computing the answers to Q. We also illustrate some experiments showing that, in practice, SBP is significantly more efficient than the previous approach.

ABSTRACT. We investigate cases where an ontology expressed in a seemingly hard DL can be polynomially reduced to one in a simpler logic, while preserving classification and fact entailment reasoning outcomes. Our transformations target the elimination of inverse roles, universal and existential restrictions, and in the best case allow us to rewrite the given ontology into one of the OWL 2 profiles. Even if an ontology cannot be fully rewritten into a profile, in many cases our transformations allow us to exploit further optimisation techniques. Moreover, the elimination of some out-of-profile axioms can improve the performance of modular reasoners, such as MORe. We have tested our techniques on both classification and data reasoning tasks with encouraging results.

ABSTRACT. We present a new procedure for ontology materialization (computing all entailed instances of every atomic concept) in which reasoning over a large ABox is reduced to reasoning over a smaller "abstract" ABox. The abstract ABox is obtained as the result of a fixed-point computation involving two stages: 1) abstraction: partition the individuals into equivalence classes based on told information and use one representative individual per equivalence class, and 2) refinement: iteratively split (refine) the equivalence classes, when new assertions are derived that distinguish individuals within the same class. We prove that the method is complete for Horn ALCHOI ontologies, that is, all entailed instances will be derived once the fixed-point is reached. We implement the procedure in a new database-backed reasoning system and evaluate it empirically on existing ontologies with large ABoxes. We demonstrate that the obtained abstract ABoxes are significantly smaller than the original ones and can be computed with few refinement steps.

ABSTRACT. The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as separation logic has made significant progress in extracting shapes from program source code. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms from object oriented programming and databases. In this paper, we attempt to bridge the conceptual gap between these two communities. Our approach is based on description logic, a widely used knowledge representation paradigm which gives a logical underpinning for diverse modeling frameworks such as UML and ER. We show how description logic can be used on top of an existing shape analysis to add content descriptions to the shapes. Technically, we assume that we have separation logic shape invariants obtained from a shape analysis tool, and requirements on the program data in terms of description logic. We show that the two-variable fragment of first order logic with counting and trees (whose decidability was proved at LICS 2013) can be used as a joint framework to embed suitable fragments of description logic and separation logic.

ABSTRACT. Revision of knowledge bases (KBs) expressed in description logics (DLs) has gained a lot of attention lately. Existing revision algorithms can be divided into two groups: model-based approaches (MBAs) and formula-based approaches (FBAs). MBAs are fine-grained and independent of the syntactical forms of KBs; however, they only work for some restricted forms of the DL-Lite family. FBAs can deal with more expressive DLs such as SHOIN, but they are syntax-dependent and not fine-grained. In this paper, we present a new method for instance-level revision of KBs. In our algorithm, a non-redundant depth-bounded model is firstly constructed for the KB to be revised; then a revision process based on justifications is carried out on this model by treating a model as a set of assertions; finally the resulting model is mapped back to a KB which will be returned by the algorithm. Our algorithm is syntax-independent and fine-grained, and works for the DL EL_\bot.

ABSTRACT. The development and maintenance of large and complex ontologies are often time-consuming and error-prone. Thus, automated ontology learning and revision have attracted intensive research interest. In data-centric applications where the ontology is designed based on or automated learnt from the data, when new data instances are added that contradict to the ontology, it is often desirable to incrementally revise the ontology according to the added data. In this paper, we address this problem using TBox revision and allow TBox axioms to be revised by ABox assertions. To provide a model-theoretic characterisation of minimal change, we introduce and apply the type semantics for DL-Lite TBoxes. We define a concrete revision operator using the type semantics, and show that it possesses desired properties.

ABSTRACT. An essential task in managing description logic (DL) ontologies is the removal of problematic axioms. Such removal is formalised as the operation of contraction in belief change. In this paper, we investigate contraction over DL-Lite$_\R$ TBoxes so as to provide methods for eliminating problematic axioms in DL-Lite$_\R$ TBoxes. In belief change, a well known approach in defining contraction is via epistemic entrenchments which are essentially preference orderings over formulas. The approach however is not applicable in DLs as classic belief change assumes an underlying logic different from DLs. Thus we reformulate the epistemic entrenchment approach so as to make it applicable to DL-Lite$_\R$. We then provide representation theorem and a tractable algorithm for the reformulated approach.

ABSTRACT. We propose a nonmonotonic extension of SHIQ, which is at the base of the OWL-DL language and does not enjoy the finite model property. We extend to SHIQ the well established notion of rational closure, a nonmonotonic mechanism introduced by Lehmann and Magidor for propositional logic, built on the top of the rational logic R. We start from an extension of SHIQ with a typicality operator T, whose aim is to select the typical (the most normal) instances of a concept C: T(C) stands for typical Cs. As a further contribution, we provide a semantic characterization of the rational closure for SHIQ, namely a minimal model semantics built upon standard Description Logics models enriched with a preference relation among domain elements.

ABSTRACT. The preferential approach to nonmonotonic reasoning was consolidated in depth by Krause, Lehmann and Magidor (KLM) for propositional logic in the early 90’s. In recent years, there have been efforts to extend their framework to Description Logics (DLs) and a solid theoretical foundation has already been established towards this aim. Despite this foundation, and the fact that many of the desirable aspects of the approach generalise favourably to certain DLs, implementations thereof remain unpublished. We present a defeasible reasoning system for OWL ontologies demonstrating that we need not devise new decision procedures for certain preferential DLs. Our reasoning procedures are composed purely of classical DL decision steps which allows us to immediately hinge upon existing OWL and DL systems for defeasible reasoning tool support.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. EL is a family of tractable Description Logics (DLs) that is the basis of the OWL~2 EL profile. Unlike for many expressive DLs, reasoning in EL can be performed by computing a deductively-closed set of logical consequences of some specific form. In some ontology-based applications, e.g., for ontology debugging, knowing the logical consequences of the ontology axioms is often not sufficient. The user also needs to know from which axioms and how the consequences were derived. Although it is possible to keep track of all inferences applied during reasoning, this is usually not done in practice to avoid the overheads. In this paper, we present a goal-directed method that can generate inferences for selected consequences in the deductive closure without re-applying all rules from scratch. We provide an empirical evaluation demonstrating that the method is fast and economical for large EL ontologies. Although the main benefits are demonstrated for EL reasoning, the method can be easily extended to other procedures based on deductive closure computation using fixed sets of rules.

ABSTRACT. Developing and maintaining ontologies is an expensive and error-prone task. After an error is detected, users may have to wait for a long time before a corrected version of the ontology is available. In the meantime, one might still want to derive meaningful knowledge from the ontology, while avoiding the known errors. We introduce brave and cautious reasoning and show that it is hard for EL. We then propose methods for improving the reasoning times by precompiling information about the known errors and using proof-theoretic techniques for computing justifications. A prototypical implementation shows that our approach is feasible for large ontologies used in practice.

ABSTRACT. Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics almost 20 years ago, motivated by applications in the Classic system. For the Description Logic EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBox that satisfy a certain restriction on cyclic dependencies between concepts, but the general case ist still open. For matching, we solve the general case in this paper: we show that matching in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented matching algorithm that uses nondeterministic rules to transform a given matching problem into a solved form by a polynomial number of rule applications. We also investigate some tractable variants of the matching problem.

ABSTRACT. Representation of context dependent knowledge in the Semantic Web has been recognized as a relevant issue: as a consequence, a number of logic based formalisms have been proposed in this regard. In response to this need, in previous works, we presented the description logic-based Contextualized Knowledge Repository (CKR) framework. Starting from this point, the first contribution of the paper is an extension of CKR with the possibility to represent defaults in context dependent axioms and a translation of extended CKRs to datalog programs with negation under answer set semantics. The translation generates datalog programs which are sound and complete w.r.t. instance checking in CKRs. Exploiting this result, we have developed as a second contribution a prototype implementation that compiles a CKR based on OWL2RL to a datalog program. Finally, we compare our approach with major non-monotonic formalisms for description logics and contextual knowledge representation.