Many AI applications rely on knowledge encoded in a locigal knowledge base (KB). The most essential benefit of such logical KBs is the opportunity to perform automatic reasoning which however requires a KB to meet some minimal quality criteria such as consistency. Without adequate tool assistance, the task of resolving such violated quality criteria in a KB can be extremely hard, especially when the problematic KB is large and complex. To this end, interactive KB debuggers have been introduced which ask a user queries whether certain statements must or must not hold in the intended domain. The given answers help to gradually restrict the search space for KB repairs. Existing interactive debuggers often rely on a pool-based strategy for query computation. A pool of query candidates is precomputed, from which the best candidate according to some query quality criterion is selected to be shown to the user. This often leads to the generation of many unnecessary query candidates and thus to a high number of expensive calls to logical reasoning services. We tackle this issue by an in-depth mathematical analysis of diverse real-valued active learning query selection measures in order to determine qualitative criteria that make a query favorable. These criteria are the key to devising efficient heuristic query search methods. The proposed methods enable for the first time a completely reasoner-free query generation for interactive KB debugging while at the same time guaranteeing optimality conditions, e.g. minimal cardinality or best understandability for the user, of the generated query that existing methods cannot realize. Further, we study different relations between active learning measures. The obtained picture gives a hint about which measures are more favorable in which situation or which measures always lead to the same outcomes, based on given types of queries.

We introduce a new family of graphical models that consists of graphs with possibly directed, undirected and bidirected edges but without directed cycles. We show that these models are suitable for representing causal models with additive error terms. We provide a set of sufficient graphical criteria for the identification of arbitrary causal effects when the new models contain directed and undirected edges but no bidirected edge. We also provide a necessary and sufficient graphical criterion for the identification of the causal effect of a single variable on the rest of the variables. Moreover, we develop an exact algorithm for learning the new models from observational and interventional data via answer set programming. Finally, we introduce gated models for causal effect identification, a new family of graphical models that exploits context specific independences to identify additional causal effects. Keywords: Acyclic directed mixed graphs; causal models; answer set programming.

This paper describes a system for automated reasoning in the dialetheic logic RM3. A dialetheic logic allows formulae to be true, or false, or (differently from classical logic) both true and false, and the connectives are interpreted in terms of these three truth values. Consequently some inference rules of classical logic are invalid in RM3, and some theorems of classical logic are not theorems of RM3. An automated theorem prover for first-order RM3 has been developed, based on translations of RM3 formulae to classical first-order logic, and use of existing first-order reasoning systems to reason over the translated formulae. Examples and results are provided to highlight the differences between reasoning in RM3 and classical logic.

Each of these areas already features a significant level of complexity, so the following description of data mining and artificial intelligence applications has necessarily been restricted to an overview. Vehicle development has become a largely virtual process that is now the accepted state of the art for all manufacturers. CAD models and simulations (typically of physical processes, such as mechanics, flow, acoustics, vibration, etc., on the basis of finite element models) are used extensively in all stages of the development process. The subject of optimization (often with the use of evolution strategies[31] or genetic algorithms and related methods) is usually less well covered, even though it is precisely here in the development process that it can frequently yield impressive results. Multi-disciplinary optimization, in which multiple development disciplines (such as occupant safety and noise, vibration, and harshness (NVH)) are combined and optimized simultaneously, is still rarely used in many cases due to supposedly excessive computation time requirements.

In 1931 at the age of just 25 years, the young Austrian mathematician Kurt Goedel proved an astonishing mathematical theorem that made him instantly famous and a celebrity in mathematical circles around the world (see picture; in the Anglo-Saxon literature Goedel is usually referred to as "Godel" skipping the Umlaut in his German name). Despite its very abstract nature and the lack of any every day practical use, Goedel's theorem - the so called Incompleteness Theorem - has had a dramatic and deep impact on mathematics itself and its foundations. It also had a substantial impact on the philosophy of the 20th century and our understanding of the general limitations of computers and algorithms. I will explain here how Goedel's theorem actually caused the emergence of the new science of Artificial Intelligence (AI) and theoretical computer science in the 1940s and 1950s and how it motivated such key AI pioneers like Alan Turing to get involved. The birth of AI and the course AI has taken ...

First-Order Logic (FOL) is widely regarded as one of the most important foundations for knowledge representation. Nevertheless, in this paper, we argue that FOL has several critical issues for this purpose. Instead, we propose an alternative called assertional logic, in which all syntactic objects are categorized as set theoretic constructs including individuals, concepts and operators, and all kinds of knowledge are formalized by equality assertions. We first present a primitive form of assertional logic that uses minimal assumed knowledge and constructs. Then, we show how to extend it by definitions, which are special kinds of knowledge, i.e., assertions. We argue that assertional logic, although simpler, is more expressive and extensible than FOL. As a case study, we show how assertional logic can be used to unify logic and probability, and more building blocks in AI.

Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however.

According to Clark's seminal work on common ground and grounding, participants collaborating in a joint activity rely on their shared information, known as common ground, to perform that activity successfully, and continually align and augment this information during their collaboration. Similarly, teams of human and artificial agents require common ground to successfully participate in joint activities. Indeed, without appropriate information being shared, using agent autonomy to reduce the workload on humans may actually increase workload as the humans seek to understand why the agents are behaving as they are. While many researchers have identified the importance of common ground in artificial intelligence, there is no precise definition of common ground on which to build the foundational aspects of multi-agent collaboration. In this paper, building on previously-defined modal logics of belief, we present logic definitions for four different types of common ground. We define modal logics for three existing notions of common ground and introduce a new notion of common ground, called salient common ground. Salient common ground captures the common ground of a group participating in an activity and is based on the common ground that arises from that activity as well as on the common ground they shared prior to the activity. We show that the four definitions share some properties, and our analysis suggests possible refinements of the existing informal and semi-formal definitions.

Logic rules and inference are fundamental in computer science, especially for solving complex modeling, reasoning, and analysis problems in critical areas such as program verification, security, and decision support. The semantics of logic rules and their efficient computations have been a subject of significant study, especially for complex rules that involve recursive definitions and unrestricted negation and quantifications. Many different semantics and computation methods have been proposed. Even the two dominant semantics for logic programs, well-founded semantics (WFS) [VRS91, VG93] and stable model semantics (SMS) [GL88], are still difficult to understand intuitively, even for extremely simple rules; they also make implicit assumptions and, in some cases, do not capture common sense, especially ignorance. This paper describes a simple new semantics for logic rules, founded semantics, that extends straightforwardly to another simple new semantics, constraint semantics.

What inspired you to study Artificial Intelligence? I did my first degree at Imperial College in computer science; in my final year, I took a module in Logic Programming which was taught by Professor Robert Kowalski. It was fascinating because it was so different to other things I'd learned; it featured a declarative form of programming that allowed the system to "reason" and provide its own conclusions. Indeed, this was so fascinating for me that I wrote a connection graph theorem prover in Prolog for my final year project; I then went on to study Artificial Intelligence at the University of Edinburgh. I remain fascinated by systems that permit you to say things at a high level of abstraction and then allow systems to draw their own conclusions. What were your initial main challenges when you began to study Artificial Intelligence?