ABSTRACT. While the fields of KR and computer vision have diverged since the early days of AI, there have been recent moves to re-integrate these fields. I will talk about some of this work, focusing on research from Leeds on building models of video activity from video input. I will present techniques, both supervised and unsupervised, for learning the spatiotemporal structure of tasks and events from video or other sensor data, particularly in the case of scenarios with concurrent activities. The representations exploit qualitative spatio-temporal relations which have been an active area of research in KR for a number of years. I will also talk about the problem of robustly computing symbolic descriptions from noisy video data. Finally, I will show how objects can be functionally categorised according to their spatiotemporal behaviours.

ABSTRACT. In this paper, we prove the decidability of stable model reasoning with guarded existential rules where rule bodies may contain negated atoms, as well as for reasoning using rules of the corresponding fragment of guarded Datalog+/-. In addition, we provide complexity results for these reasoning tasks (including conjunctive query answering) for a number of settings. Given that several lightweight description logics (in particular, DL-Lite, ELH, and OWL QL) can be directly translated to guardede Datalog+/-, we herewith obtain a direct stable model semantics for several description logics (DLs). This allows us to use negation (or complementation) directly in the axioms of a TBox, and to obtain a clear and natural semantics for such theories via their simple translation into an answer set program. We refer to this approach as to the "direct" stable model semantics in contrast to previous hybrid approaches that combine logic programming primitives with DL constructs, where the latter can be embedded into an answer set logic program, similar to generalized quantifiers (for example, the so-called dl-programs by Eiter et al. KR 2004; AIJ 2008).

ABSTRACT. We develop a clausal resolution-based approach for computing uniform interpolants of TBoxes formulated in the description logic ALC when such uniform interpolants exist. We also present an experimental evaluation of our approach and of its application to the logical difference problem for real-life ALC ontologies. Our results indicate that in many practical cases uniform interpolants exist and that they can be computed with the presented algorithm.

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 is known about their computational complexity and expressivity. We close this gap by providing a comprehensive analysis 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. Our proofs employ general modeling techniques that exploit the power of nominal schemas to succinctly represent many axioms, and which can also be applied to study DLs beyond those we consider. 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. In the last few years there has been a large effort for analysing the computational properties of reasoning in fuzzy Description Logics. This has led to a number of papers studying the complexity of these logics, depending on their chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy DLs w.r.t. witnessed models over the Goedel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in this logic in exponential time, matching the complexity of reasoning in classical ALC.

ABSTRACT. Golog and ConGolog are languages defined in the situation calculus for cognitive robotics. Given a Golog program P, its semantics is defined by a macro Do(P,s,s') that expands to a logical sentence that captures the conditions under which performing P in s can terminate in s'. A similar macro is defined for ConGolog programs. In general, the logical sentences that these macros expand to are second-order, and in the case of ConGolog, may involve quantification over programs. In this paper, we show that by making use of the foundational axioms in the situation calculus, these macro expressions can actually be defined using first-order sentences.

ABSTRACT. When Lin and Reiter introduced the progression of basic action theories in the situation calculus, they were essentially motivated by long-lived robotic agents functioning over thousands of actions. However, their account does not deal with probabilistic uncertainty about the initial situation nor with effector or sensor noise, as needed in robotic applications. In this paper, we obtain results on how to progress continuous degrees of belief against continuous effector and sensor noise in a semantically correct fashion. Most significantly, and perhaps surprisingly, we identify conditions under which our account is not only as efficient as the filtering mechanisms commonly used in robotics, but considerably more general.

ABSTRACT. Among the most frequent reasoning tasks in the situation calculus are projection queries that query the truth of conditions in a future state of affairs. However, in long running action sequences solving the projection problem is complex. The main contribution of this work is a new technique which allows the length of the action sequences to be reduced by reordering independent actions and removing dominated actions; maintaining semantic equivalence with respect to the original action theory. This transformation allows for the removal of actions that are problematic with respect to progression, allowing for periodical update of the action theory to reflect the current state of affairs. We provide the logical framework for the general case and give specific methods for two important classes of action theories. The work provides the basis for handling more expressive cases, such as the reordering of sensing actions in order to delay progression, and forms an important step towards facilitating ongoing planning and reasoning by long-running agents. It provides a mechanism for minimising the need for keeping the action history while appealing to both regression and progression.

ABSTRACT. In this paper we develop a general framework that allows for both knowledge acquisition and forgetting in the Situation Calculus. Based on the Scherl and Levesque possible worlds approach to knowledge in the Situation Calculus, we allow for both sensing as well as explicit forgetting actions to take place. This model of forgetting is then compared to existing frameworks, particularly showing that forgetting is well-behaved with respect to the contraction operator of the well-known AGM theory of belief revision.

ABSTRACT. The standard way of answering queries over incomplete databases is to compute certain answers to them. These have always been defined as the intersection of query answers on all complete databases that are represented by the incomplete database. But is this universally accepted definition correct? Our goal is to argue that this `one-size-fits-all' definition can often lead to counterintuitive or just plain wrong results, and to propose an alternative framework for defining certain answers.

The idea of the framework is to move away from the standard, in the database literature, assumption that query results be given in the form of a database object, and to allow instead two alternative representations of answers: as objects defining all other answers, or as knowledge we can deduce with certainty about all such answers. We show that the latter is often easier to achieve than the former, that in general certain answers need not be defined as intersection, and may well contain missing information in them. We also show that with a proper choice of semantics, we can often reduce computing certain answers - as either objects or knowledge - to standard query evaluation. We describe the framework in the most general way, applicable to a variety of data models, and test it on three concrete relational semantics of incompleteness: open, closed, and weak closed world.

ABSTRACT. We study disambiguating of pronoun references in Winograd Schemas, which are part of the Winograd Schema Challenge, a proposed replacement for the Turing test. In particular we consider sentences where the pronoun can be resolved to both antecedents without semantic violations in world knowledge, that means for both readings of the sentence there is a possible consistent world. Nevertheless humans will strongly prefer one answer, which can be explained by pragmatic effects described in Relevance Theory. We state formal optimization criteria based on principles of Relevance Theory in a simplification of Roger Schank's graph framework for natural language understanding. We perform experiments using Answer Set Programming and report the usefulness of our criteria for disambiguation and their sensitivity to parameter variations.

ABSTRACT. Agents in real-world environments may have only \emph{partial} access to available information, often in an arbitrary, or hard to model, manner. By reasoning with knowledge at their disposal, agents may hope to recover some missing information. By acquiring the knowledge through a process of learning, the agents may further hope to guarantee that the recovered information is indeed correct.

Assuming only a black-box access to a learning process and a prediction process that are able to cope with missing information in some principled manner, we examine how the two processes should interact so that they improve their overall joint performance. We identify natural scenarios under which the interleaving of the processes is provably beneficial over their independent use.

ABSTRACT. We present a cognitive design assistance system equipped with analytical capabilities aimed at anticipating architectural building design performance with respect to people-centred functional design goals. The paper focuses on the system capability to generate \emph{narratives of visuo-locomotive user experience} from digital computer-aided architecture design (CAAD) models. The system is based on an underlying declarative narrative representation and computation framework pertaining to conceptual, geometric, and qualitative spatial knowledge. The semantics of the declarative narrative model, i.e., the overall representation and computation model, is founded on: (a) conceptual knowledge formalised in an OWL ontology; (b) a general spatial representation and reasoning engine implemented in constraint logic programming; and (c) a declaratively encoded (narrative) construction process (over graph structures) implemented in answer-set programming.

We emphasise and demonstrate: complete system implementation, algorithmic scalability, and robust performance \& integration with industry-scale architecture industry tools (e.g., Revit, ArchiCAAD) \& standards (BIM, IFC).

ABSTRACT. This paper presents Tweety, an open source project for scientific experimentation on logical aspects of artificial intelligence and particularly knowledge representation. Tweety provides a general framework for implementing and testing knowledge representation formalisms in a way that is familiar to researchers used to logical formalizations. This framework is very general, widely applicable, and can be used to implement a variety of knowledge representation formalisms from classical logics, over logic programming and computational models for argumentation, to probabilistic modeling approaches. Tweety already contains over 15 different knowledge representation formalisms and allows easy computation of examples, comparison of algorithms and approaches, and benchmark tests. This paper gives an overview on the technical architecture of Tweety and a description of its different libraries. We also provide two case studies that show how Tweety can be used for empirical evaluation of different problems in artificial intelligence.

ABSTRACT. In this paper we present SmartPM, a model and a prototype Process Management System featuring a set of techniques providing support for automatic adaptation of knowledge-intensive processes at run-time. Such techniques are able to automatically adapt process instances without explicitly defining policies to recover from exceptions and without the intervention of domain experts at run-time, aiming at reducing error-prone and costly manual ad-hoc changes, and thus at relieving users from complex adaptations tasks. To accomplish this, we make use of well-established techniques and frameworks from Artificial Intelligence, such as situation calculus, Indigolog and classical planning.

ABSTRACT. Diagnostic problem solving involves a myriad of reasoning tasks associated with the determination of diagnoses, the generation and execution of tests to discriminate diagnoses, and the determination and execution of actions to alleviate symptoms and/or their root causes. Fundamental to diagnostic problem solving is the need to reason about action and change. In this work we explore these myriad of reasoning tasks through the lens of AI automated planning. We characterize a diversity of reasoning tasks associated with diagnostic problem solving, prove properties of these characterizations, and define correspondences with established automated planning tasks and existing state-of-the-art planning systems. In doing so, we provide deeper insight into the computational challenges associated with diagnostic problems solving, as well as proposing practical algorithms for their realization.

ABSTRACT. We consider the problem of representing and reasoning about computer programs, and propose a translator from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the ``less than'' linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare's logic, our approach does not rely on loop invariants. Unlike typical temporal logic specification of programs, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.

ABSTRACT. In this paper we present a tableau-based method to decide the satisfiability of formulas in ATEL, an extension of the alternating-time temporal logic ATL including epistemic modalities for individual knowledge. Specifically, we analyse satisfiability of ATEL formulas under a number of conditions. We evaluate the impact of the assumptions of synchronicity and of a unique initial state, which have been proposed in the context of Interpreted Systems. Also, we consider satisfiability at a initial state as opposed to any state in the system. We introduce a tableau-based decision procedure for each of these combinations. Moreover, we adopt an agent-based approach to satisfiability, namely, the decision procedure returns a set of agents inducing a concurrent game structure that satisfies the specification at hand.

ABSTRACT. Inconsistency measures help analyzing contradictory knowledge bases and resolving inconsistencies. In recent years several measures with desirable properties have been proposed, but often these measures correspond to combinatorial or non-convex optimization problems that are hard to solve in practice. In this paper, I study a new family of inconsistency measures for probabilistic knowledge bases. All members satisfy many desirable properties and can be computed by means of convex optimization techniques. For two members, I present linear programs whose computation is barely harder than a probabilistic satisfiability test.

ABSTRACT. Graphical belief models are compact and powerful tools for representing and reasoning under uncertainty. Possibilistic networks are graphical belief models based on possibility theory. In this paper, we address reasoning under uncertain inputs in both quantitative and qualitative possibilistic networks. More precisely, we first provide possibilistic counterparts of Pearl's methods of virtual evidence then compare them with the possibilistic counterparts of Jeffrey's rule of conditioning. As in the probabilistic setting, the two methods are shown to be equivalent in the quantitative setting regarding the existence and uniqueness of the solution. However in the qualitative setting, Pearl's method of virtual evidence which applies directly on graphical models disagrees with Jeffrey's rule and the virtual evidence method. The paper provides the precise situations where the methods are not equivalent. Finally, the paper addresses related issues like transformations from one method to another and commutativity.

ABSTRACT. Logistic regression is a commonly used representation for aggregators in Bayesian belief networks when a child has multiple parents. Variations of population, as well as a desire to model interactions between parents in relational models, introduce representational problems for using logistic regression in relational models. In this paper, we first examine the representational problems caused by population variation. We show how these problems arise even in simple cases with a single parametrized parent, and propose a linear relational logistic regression which we show can represent arbitrary linear (in population size) decision thresholds, where the traditional logistic regression cannot. Then we examine representing interactions between parents of a child node, and representing non-linear dependency on population size. We propose a multi-parent relational logistic regression which can represent interactions between parents and arbitrary polynomial decision thresholds. Finally, we show how other well-known aggregators can be represented using this relational logistic regression.

ABSTRACT. In 2001 Ray Reiter published his seminal book, Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The book represented the culmination of 10 years of work by Reiter and his many collaborators investigating, formalizing, and extending the situation calculus, first introduced by John McCarthy in 1963 as a way of logically specifying dynamical systems. While researchers continue to extend the situation calculus, it has also seen significant scientific deployment to aid in the specification and implementation of a diversity of automated reasoning endeavors including diagnosis, web services composition and customization, and nonclassical automated planning. In this talk I will examine the important role the situation calculus has more recently been playing in explicating nuances in the logical specification and realization of some of these diverse automated reasoning tasks.