View: session overviewtalk overviewside by side with other conferences
10:45  Invited Talk: New Perspectives on Query Reformulation SPEAKER: Michael Benedikt 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 veryrecent 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 costbased query optimization to the setting of constraintbased 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. 
11:45  Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs SPEAKER: Michael Morak 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 EXPTIMEhard. This result together with an EXPTIME upper bound obtained by exploiting classical results on guarded firstorder 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 DLLite_{bool}^{H}, one of the most expressive languages of the DLLite family of DLs, is EXPTIMEcomplete, even in the case of a fixed TBox. In fact, the EXPTIMEhardnees holds even for DLLite_{bool}, that is, the DL obtained from DLLite_{bool}^{H} after forbidding role hierarchies. 
12:10  Complexities of Nominal Schemas SPEAKER: unknown ABSTRACT. Nominal schemas extend description logics (DLs) with a restricted form of variables, thus integrating rulelike 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. 
12:35  Comparing the Expressiveness of Description Logics SPEAKER: Ali Rezaei Divroodi 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. 
12:38  An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies SPEAKER: unknown 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. 
12:41  Predicting OWL Reasoners: Locally or Globally? SPEAKER: unknown 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. 
12:44  Bridging the Gap between Tableau and ConsequenceBased Reasoning SPEAKER: unknown ABSTRACT. We present a nondeterministic consequencebased procedure for the description logic ALCHI. Just like the similar style (deterministic) procedures for EL and HornSHIQ, our procedure explicitly derives subsumptions between concepts, but due to nondeterministic 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 tableaubased 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. 
12:47  Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability SPEAKER: Tomer Kotek ABSTRACT. Program Analysis requires expressive logics enjoying good computational properties and capable of describing graphstructured 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 firstorder 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 polynomialtime reducible to finite satisfiability of $ALCQIO$formulae. As a consequence, we get that finite satisfiability and finite implication in $ALCQIO_{b,Re}$ are NEXPTIMEcomplete. Extensions of DLs with reachability have been studied previously (mainly in terms of fixpoints 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. 
12:50  How to Best Nest Regular Path Queries SPEAKER: unknown ABSTRACT. Regular path queries (RPQs) define query patterns in terms of regular expressions and are therefore wellsuited to query for paths over roles in DL. RPQs can be extended to 2way 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 nonelementary in the worst case, with an exponential increase for each level of nesting. 
12:53  Typed HigherOrder Variant of SROIQ  Why Not? SPEAKER: unknown 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 higherorder 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. 
12:56  Practical query answering over Hi (DLLiteR) knowledge bases SPEAKER: unknown ABSTRACT. The language Hi(DLLiteR) is obtained from DLLiteR by adding metamodeling features, and is equipped with a query language that is able to express higherorder queries. We investigate the problem of answering a particular class of such queries, called instance higherorder queries posed over Hi (DLLiteR ) knowledge bases (KBs). The only existing algorithm for this problem is based on the idea of reducing the evaluation of a higherorder query Q over a Hi(DLLiteR) KB to the evaluation of a union of firstorder queries over a DLLiteR 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 firstorder 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. 
14:30  Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs SPEAKER: unknown 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 outofprofile 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. 
14:55  Abstraction Refinement for Ontology Materialization SPEAKER: TrungKien Tran 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 fixedpoint 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 fixedpoint is reached. We implement the procedure in a new databasebacked 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. 
15:20  Shape and Content: Incorporating Domain Knowledge into Shape Analysis SPEAKER: Tomer Kotek ABSTRACT. The verification community has studied dynamic data structures primarily in a bottomup 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 twovariable 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. 
15:45  An ABox Revision Algorithm for the Description Logic EL_\bot SPEAKER: Uli Sattler 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: modelbased approaches (MBAs) and formulabased approaches (FBAs). MBAs are finegrained and independent of the syntactical forms of KBs; however, they only work for some restricted forms of the DLLite family. FBAs can deal with more expressive DLs such as SHOIN, but they are syntaxdependent and not finegrained. In this paper, we present a new method for instancelevel revision of KBs. In our algorithm, a nonredundant depthbounded 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 syntaxindependent and finegrained, and works for the DL EL_\bot. 
15:48  Instancedriven TBox Revision in DLLite SPEAKER: unknown ABSTRACT. The development and maintenance of large and complex ontologies are often timeconsuming and errorprone. Thus, automated ontology learning and revision have attracted intensive research interest. In datacentric 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 modeltheoretic characterisation of minimal change, we introduce and apply the type semantics for DLLite TBoxes. We define a concrete revision operator using the type semantics, and show that it possesses desired properties. 
15:51  Rational Elimination of DLLite TBox Axioms SPEAKER: unknown 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 DLLite$_\R$ TBoxes so as to provide methods for eliminating problematic axioms in DLLite$_\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 DLLite$_\R$. We then provide representation theorem and a tractable algorithm for the reformulated approach. 
15:54  Rational closure in SHIQ SPEAKER: unknown ABSTRACT. We propose a nonmonotonic extension of SHIQ, which is at the base of the OWLDL 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. 
15:57  DIP: A DefeasibleInference Platform for OWL Ontologies SPEAKER: unknown 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. 
16:30  Foundations and Technology Competitions Award Ceremony 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:
The following three Boards of Jurors were in charge of choosing the winners:
http://fellowship.logic.at/ 
17:30  FLoC Olympic Games Award Ceremony 1 SPEAKER: Floc Olympic Games 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

18:15  FLoC Closing Week 1 SPEAKER: Helmut Veith 
16:50  GoalDirected Tracing of Inferences in EL Ontologies SPEAKER: unknown 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 deductivelyclosed set of logical consequences of some specific form. In some ontologybased 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 goaldirected method that can generate inferences for selected consequences in the deductive closure without reapplying 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. 
17:15  Brave and Cautious Reasoning in EL SPEAKER: Rafael Peñaloza ABSTRACT. Developing and maintaining ontologies is an expensive and errorprone 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 prooftheoretic techniques for computing justifications. A prototypical implementation shows that our approach is feasible for large ontologies used in practice. 
17:40  Matching with respect to general concept inclusions in the Description Logic EL SPEAKER: unknown 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 NPcomplete. It then took almost 10 years before this NPcompleteness 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 NPcomplete by introducing a goaloriented 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. 
18:05  Contextualized Knowledge Repositories with Justifiable Exceptions SPEAKER: Loris Bozzato 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 logicbased 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 nonmonotonic formalisms for description logics and contextual knowledge representation. 