ABSTRACT. We consider the scenario of ontology-based data access where a conjunctive query is evaluated against an ontological database. It is generally accepted that true scalability of conjunctive query answering in this setting can only be achieved by using standard relational database management systems (RDBMSs). An approach to conjunctive query answering that enables the use of RDBMSs is the so-called polynomial combined approach. We investigate this approach for the main guarded- and sticky-based classes of existential rules, and we highlight the assumptions on the underlying schema which are sufficient for the polynomial combined first-order rewritability of those classes. To the best of our knowledge, this is the first work which explicitly studies the polynomial combined approach for existential rules.

ABSTRACT. Two-way regular path queries (2RPQs) have received increased attention recently due to their ability to relate pairs of objects by flexibly navigating graph structured data. They are present in property paths in SPARQL 1.1, the new standard RDF query language, and in the XML query language XPath. In line with XPath, we consider the extension of 2RPQs with nesting, which allows one to require that objects along a path satisfy complex conditions, in turn expressed through (nested) 2RPQs. We study the computational complexity of answering nested 2RPQs and conjunctions thereof (CN2RPQs) in the presence of domain knowledge expressed in description logics (DLs). We establish tight complexity bounds in data and combined complexity for a variety of DLs, ranging from lightweight DLs (DL-Lite, EL) up to highly expressive ones. Interestingly, we are able to show that adding nesting to (C)2RPQs does not affect worst-case data complexity of query answering for any of the considered DLs. However, in the case of lightweight DLs, adding nesting to 2RPQs leads to a surprising jump in combined complexity, from P-complete to ExpTime-complete.

ABSTRACT. We investigate conjunctive query inseparability of description logic (DL) knowledge bases (KBs) w.r.t. a given signature, a fundamental problem for KB versioning, module extraction, forgetting and knowledge exchange. We study the data and combined complexity of deciding KB query inseparability for fragments of Horn-ALCHI, including the DLs underpinning OWL 2 QL and OWL 2 EL. While all of these DLs turn out to be P-complete for data complexity, the combined complexity ranges from P to EXPTIME and 2EXPTIME. We also resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal UCQ solutions in knowledge exchange are both EXPTIME-complete for combined complexity.

ABSTRACT. In Description Logic (DL) knowledge bases (KBs) information is typically captured by crisp concepts. For many applications, querying the KB by crisp query concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of concept similarity measures. In this paper we formalize the task of instance query answering for crisp DL KBs using concepts relaxed by concept similarity measures. We investigate computation algorithms for this task in the DL EL, their complexity and properties for the employed similarity measure regarding whether unfoldable or general TBoxes are used.

ABSTRACT. The study of extension-based semantics within the seminal abstract argumentation model of Dung has largely focused on definitional, algorithmic and complexity issues. In contrast, matters relating to comparisons of representational limits, in particular, the extent to which given collections of extensions are expressible within the formalism, have been under-developed. As such, little is known concerning conditions under which a candidate set of subsets of arguments are “realistic” in the sense that they correspond to the extensions of some argumentation framework AF for a semantics of interest. In this paper we present a formal basis for examining extension-based semantics in terms of the sets of extensions that these may express within a single AF. We provide a number of characterization theorems which guarantee the existence of AFs whose set of extensions satisfy specific conditions and derive preliminary complexity results for decision problems that require such characterizations.

ABSTRACT. In this paper, we investigate the revision of argumentation systems à la Dung. We focus on revision as minimal change of the arguments status. Contrarily to most of the previous works on the topic, the addition of new arguments is not allowed in the revision process, so that the revised system has to be obtained by modifying the attack relation only. We introduce a language of revision formulae which is expressive enough for enabling the representation of complex conditions on the acceptability of arguments in the revised system. We show how AGM belief revision postulates can be translated to the case of argumentation systems. We provide a corresponding representation theorem in terms of minimal change of the arguments statuses. Several distance-based revision operators satisfying the postulates are also pointed out, along with some methods to build revised argumentation systems. We also discuss some computational aspects of those methods.

ABSTRACT. This paper presents a meta-algorithm, based on the general recursive schema for argumentation semantics called SCC-Recursiveness, for the computation of preferred labellings. The idea is to recursively decompose a framework so as to compute semantics labellings on restricted sub-frameworks, in order to reduce the computational effort. The meta-algorithm can be instantiated with a specific "base algorithm", applied to the base case of the recursion, which can be obtained by generalizing existing algorithms in order to compute labellings in restricted sub-frameworks. We devise to this purpose a generalization of a SAT-based state-of-the art algorithm, and provide an empirical investigation to show the significant improvement of performances obtained by exploiting the SCC-recursive schema.

ABSTRACT. We provide a logical analysis of abstract argumentation frameworks and their dynamics. Following previous work, we express attack relation and argument status by means of propositional variables and define acceptability criteria by formulas of propositional logic. We here study the dynamics of argumentation frameworks in terms of basic operations on these propositional variables, viz. change of their truth values. We describe these operations in a uniform way within a well-known variant of Propositional Dynamic Logic PDL: the Dynamic Logic of Propositional Assignments, DL-PA. The atomic programs of DL-PA are assignments of propositional variables to truth values, and complex programs can be built by means of the connectives of sequential and nondeterministic composition and test. We start by showing that in DL-PA, the construction of extensions can be performed by a DL-PA program that is parametrized by the definition of acceptance. We then mainly focus on how the acceptance of one or more arguments can be enforced and show that this can be achieved by changing the truth values of the propositional variables describing the attack relation in a minimal way.

ABSTRACT. Identity relations are at the foundation of many logic-based knowledge representations. We argue that the traditional notion of equality, based on Leibniz’ principle of indiscernability, is unsuited for many realistic knowledge representation settings. The classical interpretation of equality is simply too strong when the equality statements are re-used outside their original context.

The most prominent modern example of such re-use of knowledge across contexts is the Linked Open Data initiative, and the SemanticWeb in general. On the SemanticWeb, equality statements are used to interlink multiple descriptions of the same object, using owl:sameAs assertions. And indeed, many practical uses of owl:sameAs are known to violate the formal Leibniz-style semantics.

First, we survey the problems with the classical definition of identity, both in general, and on the Semantic Web in particular. In order to provide a more flexible semantics to identity, we then propose a method that assigns meaning to the subrelations of an identity relation using the predicates that are used in a knowledge-base. Using those indiscernabilitypredicates, we define upper and lower approximations of equality in the style of rought-set theory, resulting in a quality-measure for the identity relation.

We illustrate our approach on a realistic Semantic Web dataset, and we experimentally verify that our approach yields the intuitively desired results on this dataset.

ABSTRACT. We propose a novel approach to performance prediction of OWL reasoners. The existing strategies take a view of an entire ontology corpus: they extract multiple features from the ontologies in the corpus and use them for training machine learning models. We call these global approaches. In contrast, our approach is a local one: it examines a single ontology (independent of any corpus), selects suitable, small ontology subsets, and extrapolates their performance measurements to the whole ontology. Our results show that this simple idea leads to accurate performance predictions, comparable or superior to global approaches. Our second contribution concerns ontology features: we are the first to investigate intercorrelation of ontology features using Principal Component Analysis (PCA). We report that extracting multiple features - as global approaches do - makes surprisingly little difference for performance prediction. In fact, it turns out that the ontologies in two major corpora basically only differ in one or two features.

ABSTRACT. Several researchers have developed properties that ensure compatibility of a concept similarity or dissimilarity measure with the formal semantics of Description Logics. While these authors have highlighted the relevance of the triangle inequality, none of their proposed dissimilarity measures satisfies it. In this work we present several dissimilarity measures with this property: first, a simple dissimilarity measure, based on description trees for the lightweight Description Logic EL; secondly, a general framework based on concept relaxations; last, an instantiation of the general framework using dilation operators from mathematical morphology, exploiting the link between Hausdorff distance and dilations using balls of the ground distance as structuring elements. A comparison between these definitions and their properties is provided as well.

ABSTRACT. Given a set of conflicting arguments, there can exist multiple plausible opinions about which arguments should be accepted, rejected, or deemed undecided. Recent work explored some operators for deciding how multiple such judgments should be aggregated. Here, we generalize this line of study by introducing a family of operators called *interval aggregation methods*, and show that they contain existing operators as instances. While these methods fail to output a complete labelling in general, we show that it is possible to *transform* a given aggregation method into one that *does* always yield collectively rational labellings. This employs the *down-admissible* and *up-complete* constructions of Caminada and Pigozzi. For interval methods, collective rationality is attained at the expense of a strong *Independence* postulate, but we show that an interesting weakening of the Independence postulate is retained by this transformation. Our results open up many new directions in the study of generalized judgment aggregation in argumentation

ABSTRACT. We contribute to the study of the meta-logical properties of argumentation frameworks, as introduced by Dung. Such frameworks are used in a variety of contexts in contemporary AI, not just as a means to model argumentative scenarios, but also as an abstract mathematical representation of non-monotonic reasoning patterns more generally. Importantly, Dung observed that by representing such patterns by directed graphs, various semantics for non-monotonic reasoning could be formulated in graph theoretic terms. In this paper we address so-called sceptical reasoning about argumentation frameworks, asking the following question: what are the propositional validities of abstract argumentation? We answer this by giving graph constructions demonstrating that the set of validities for a range of different argumentation semantics coincide and that it is axiomatized by three-valued Lukasiewicz logic.

ABSTRACT. This paper brings together the theory of argumentation in AI with the psychology of story comprehension to develop a KR\&R framework for narrative text comprehension. The proposed framework is based on a computational interpretation of the general psychological principles of coherency and cognitive economy for text comprehension. Part of a wider study, this paper concentrates on the central problem of integration (or elaboration) of explicit information from the text with implicit (in the reader's mind) common sense world knowledge pertaining to the topic(s) of the story. We show how some of the major challenges for successful story comprehension are closely related to those of NMR, as found in Default Reasoning and Reasoning about Action and Change, and more specifically Knowledge Qualification and Revision. We show how an appropriate formulation through argumentation can give a basis for automating the construction and revision of a coherent comprehension model of a narrative. We report on a first set of empirical experiments designed to harness the implicit world knowledge used by humans reading a story to guide the background knowledge given as input to our framework. We present a prototype system that is used to evaluate the ability of our approach to capture both the majority and the variability of understanding of a story by the human readers in the experiment.

ABSTRACT. We introduce an abstraction methodology for the verification of multi-agent systems against specifications in alternating time temporal logic (ATL). Inspired by methodologies such as predicate abstraction, we define a three-valued semantics for the interpretation of ATL formulas on concurrent game structures and compare it to the standard two-valued semantics. We define abstract models and establish preservation results on the three-valued semantics between abstract models and their concrete counterparts. We illustrate the methodology on the large state spaces resulting from a card game.

ABSTRACT. Our aim is to develop techniques for reasoning about game-like concurrent systems, where the components of the system act rationally and strategically in pursuit of logically-specified goals. We first present a computational model for such systems, and investigate its properties. We then define and investigate a branching-time logic for reasoning about the equilibrium properties of such systems. The key operator in this logic is a path quantifier [NE]phi, which asserts that phi holds on all Nash equilibrium computations of the system.

ABSTRACT. The paper presents an extension of temporal epistemic logic with epistemic operators that capture what agents could deduce from knowledge of the strategies of some subset of the set of agents. Some examples are presented to motivate the framework, and relationships to several variants of alternating temporal epistemic logic are discussed. Results on model checking the logic are then presented.

ABSTRACT. A central result in the AGM framework for belief revision is the construction of revision functions in terms of total preorders on possible worlds. These preorders encode comparative plausibility: r <= r' states that the world r is at least as plausible as r'. Indifference in plausibility, denoted r ~ r', is defined as r ~ r' iff r <= r' and r' <= r. Herein we take a closer look at plausibility indifference. We contend that the transitivity of indifference assumed in the AGM framework is not, in general, an intuitive property for comparative plausibility. Our argument originates from similar concerns in preference modelling, where a structure weaker than a total preorder, called a semiorder, is widely consider to be a more adequate model of preference. In this paper we essentially re-construct revision functions using semiorders instead of total preorders. We formulate postulate to characterise this new, wider, class of revision functions, and prove that the postulates are soundness and completeness with respect to the semiorders-based construction. Moreover, through the Levi and Harper Identities, we characterise axiomatically the corresponding class of contraction functions.

ABSTRACT. Belief merging aims at defining the beliefs of a group from the beliefs of each member of the group. It is related to more general notions of aggregation from economy (social choice theory). Two main subclasses of belief merging operators exist: majority operators which are related to utilitarianism, and arbitration operators which are related to egalitarianism. Though utilitarian (majority) operators have been extensively studied so far, there is much less work on egalitarian operators. In order to fill the gap, we investigate possible translations in a belief merging framework of some egalitarian properties and concepts coming from social choice theory, such as Sen-Hammond equity, Pigou-Dalton property, median, and Lorenz curves. We study how these properties interact with the standard rationality conditions considered in belief merging. Among other results, we show that the distance-based merging operators satisfying Sen-Hammond equity are mainly those for which leximax is used as the aggregation function.

ABSTRACT. In the middle of the 1980s, David Poole introduced a semantical, model-theoretic notion of specificity to the artificial-intelligence community. Since then it has found further applications in non-monotonic reasoning, in particular in defeasible reasoning. Poole’s notion, however, turns out to be intricate and problematic, which — as we show — can be overcome to some extent by a closer approximation of the intuitive human concept of specificity. Besides the intuitive advantages of our novel specificity ordering over Poole’s specificity relation in the classical examples of the literature, we also report some hard mathematical facts: Contrary to what was claimed before, we show that Poole’s relation is not transitive. Our new notion of specificity is also monotonic w.r.t. conjunction.

ABSTRACT. Multi-context systems (MCSs) define a versatile framework for integrating and reasoning about knowledge from different (heterogeneous) sources. In MCSs, different types of non-monotonic reasoning are characterized by different semantics such as equilibrium semantics and grounded equilibrium semantics [Brewka and Eiter, 2007].

We introduce a novel semantics of MCSs, a supported equilibrium semantics. Our semantics is based on a new notion of support. The ``strength'' of supports determines a spectrum of semantics that, in particular, contains the equilibrium and grounded equilibrium semantics. In this way, our supported equilibrium semantics generalizes these previously defined semantics. Moreover, the ``strength'' of supports gives us a measure to compare different semantics of MCSs.

ABSTRACT. Angry Birds is a popular video game where the task is to kill pigs protected by a structure composed of different building blocks that observe the laws of physics. The structure can be destroyed by shooting the angry birds at it. The fewer birds we use and the more blocks we destroy, the higher the score. One approach to solve the game is by analyzing the structure and identifying its strength and weaknesses. This can then be used to decide where to hit the structure with the birds.

In this paper we use a qualitative spatial reasoning approach for this task. We develop a novel qualitative spatial calculus for representing and analyzing the structure. Our calculus allows us to express and evaluate structural properties and rules, and to infer for each building block which of these properties and rules are satisfied. We use this to compute a heuristic value for each block that corresponds to how useful it is to hit that block. We evaluate our approach by comparing the consequences of the suggested shot with other possible shots.

ABSTRACT. Knowledge compilation is a rewriting approach to propositional knowledge representation. The `knowledge base' is initially represented as a CNF for which many important types of queries are NP-complete to answer. Therefore, the CNF is compiled into another representation for which the minimal requirement is that the clause entailment query (can the given partial assignment be extended to a complete satisfying assignment?) can be answered in a polynomial time. Such transformation can result in exponential blow up of the representation size. A possible way to circumvent this issue is to identify a structural parameter of the input CNF such that the resulting transformation is exponential in this parameter and polynomial in the number of variables. A notable result in this direction is an $O(2^kn)$ upper bound on the size of Decomposable Negation Normal Form (DNNF) proposed by (Darwiche, JACM 2001), where $n$ is the number of variables of the given CNF and $k$ is the treewidth of its primal graph. Quite recently this upper bound has been shown to hold for Sentential Decision Diagrams (Darwiche, IJCAI2011), a subclass of DNNF that can be considered as a generalization of the famous Ordered Binary Decision Diagrams (OBDD) and shares with the OBDD the key nice features (e.g. poly-time equivalence testing). Under this parameterization, the best known upper bound for an OBDD is $O(n^k)$ (Ferrara, Pan, Vardi; LPAR2005). A natural question is whether a fixed parameter upper bound holds for OBDD.

In this paper we answer this question negatively. In particular, we demonstrate an infinite class of CNFs of the primal graph treewidth at most $k$ for which the OBDD size is at least $O(n^{k/4})/o(n)$ thus providing a separation from SDD and essentially matching the upper bound of Ferrara, Pan, and Vardi. We also establish a more optimistic version of the $O(n^k)$ upper bound for the OBDD showing that it in fact holds when $k$ is the treewidth of the incidence graph of the given CNF and thus applies for `sparse' CNFs with large clauses.

ABSTRACT. In this paper, we propose the Probabilistic Sentential Decision Diagram (PSDD), which is a canonical representation for probability distributions that are defined over the models of a propositional theory. Each parameter of a given PSDD can be viewed as the (conditional) probability of making a decision in a corresponding Sentential Decision Diagram (SDD), which itself is a recently proposed canonical representation of propositional theories. We explore a number of interesting properties of PSDDs, including the context-specific independencies that underlie them. We further show how the parameters of a PSDD can be efficiently estimated, in closed form, from complete data. We finally empirically evaluate the quality of PSDDs learned from data, when we have knowledge, a priori, of the logical theory supporting an otherwise unknown probability distribution.

ABSTRACT. Our understanding of the notion "dynamic system" is a rather broad one: such a system has states, which can change over time. Ontologies are used to describe the states of the system, possibly in an incomplete way. Monitoring is then concerned with deciding whether some run of the system or all of its runs satisfy a certain property, which can be expressed by a formula of an appropriate temporal logic. We consider different instances of this broad framework, which can roughly be classified into two cases. In one instance, the system is assumed to be a black box, whose inner working is not known, but whose states can be (partially) observed during a run of the system. In the second instance, one has (partial) knowledge about the inner working of the system, which provides information on which runs of the system are possible.

In this talk, we will review some of our recent research that investigates different instances of this general framework of ontology-based monitoring of dynamic systems. We will also sketch possible extensions towards probabilistic reasoning and the integration of mathematical modelling of dynamical systems.

ABSTRACT. The Vienna Circle of Logical Empiricism, which was part of the intellectual movement of Central European philosophy of science, is certainly one of the most important currents in the emergence of modern philosophy of science. Apart from this uncontested historical fact there remains the question of the direct and indirect influence, reception and topicality of this scientific community in contemporary philosophy of science in general as well as in the philosophy of the individual sciences, including the formal and social sciences. 

First, I will characterize the road from the Schlick-Circle to contemporary philosophy of science. Second, I will refer to "the present situation in the philosophy of science" by identifying relevant impacts, findings, and unfinished projects since the classical Vienna Circle. Third, I will address some specific European features of this globalized philosophical tradition up to the present, and outline future perspectives after the linguistic, historical and pragmatic turns – looking back to the "received view", or standard view of the Vienna Circle.

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

• Fifth Answer Set Programming Competition (ASPCOMP 2014);
• The 7th IJCAR ATP System Competition (CASC-J7);
• Hardware Model Checking Competition (HWMCC 2014);
• OWL Reasoner Evaluation (ORE 2014);
• Satisfiability Modulo Theories solver competition (SMT-COMP 2014);
• Competition on Software Verification (SV-COMP 2014);
• Syntax-Guided Synthesis Competition (SyGuS-COMP 2014);
• Synthesis Competition (SYNTCOMP 2014); and
• Termination Competition (termCOMP 2014).

ABSTRACT. Werner "Jimmy" DePauli-Schimanovich is being honored for his contributions to Gödel research, for his efforts towards re-establishing Vienna as a center of logic in the second half of the past century, and for extending the outreach of formal logic and logical thinking to other disciplines. The books about Gödel he authored, co-authored, or edited contain precious contributions of historical, philosophical, and mathematical value. His film on Gödel, and related articles and TV testimonials, attracted the general public to Gödel and his work. Moreover, DePauli-Schimanovich has unceasingly and successfully fought to re-establish logic in Vienna. He has inspired and encouraged a large number of students and young researchers, has organised meetings and social gatherings, and has created an intellectual home for scholars of logic. His activities significantly contributed to filling the intellectual vacuum in logic research that had developed in Austria in the years 1938–1945 and well into the post-war period. He was a main initiator and co-founder of the International Kurt Gödel Society. Jimmy’s research in logic involved criticism of current axiomatisations of set theory and development of new systems of naïve set theory. In informatics, DePauli-Schimanovich was co-founder and co-organiser of EuroCAST, a conference series on computer-assisted systems theory meeting alternatively in Vienna and Las Palmas, Gran Canaria. Finally, Jimmy has furthered implementation of logical ideas in disparate fields such as mechanical engineering, automated game playing, urban planning, and by inventing a number of logical games.

ABSTRACT. Zhang Mingyi is a pioneer in Artificial Intelligence and Knowledge Representation in China. He has built up a school of non-monotonic logic in Guiyang and has fostered the exchange between Chinese and Western scientists. He has contributed a large number of results on various forms of non-monotonic reasoning, including default logic, answer set programming, and belief revision. In particular, as early as 1992, he has provided important characterizations of various forms of default logic that paved the way for clarifying their computational properties and for developing algorithms for default reasoning.  Jointly with collaborators, he proposed a characterization of answer sets based on sets of generating rules, and introduced the concept of first-order loop formulas to relate answer set programming to classical logic. Other important results relate to theory revision (for example, the proof of the existence and uniqueness of finest splitting of Horn formulae) and to normal forms for Gödel logics. Many of Zhang Mingyi's former students have become internationally respected researchers.

ABSTRACT. The Free University of Bozen-Bolzano, the Technische Universität Dresden, the Universidade Nova de Lisboa, the Universidad Politécnica de Madrid (until 2010), the Technische Universität Wien, and Australia's Information Communications Technology Research Centre of Excellence (since 2007) are jointly running the European Master's Program in Computational Logic (EMCL) since 2004. The program is supported by the European Union within Erasmus Mundus and Eramsus+. So far, more than 100 students from 39 different countries have successfully completed the distributed master's program with a double or joint degree.

For the first time, the partner institutions are announcing the EMCL Distinguished Alumni Award for outstanding contributions of EMCL graduates to the field of Computational Logic.

http://www.emcl-study.eu/