Please see the Appendix of Ref. 1 for a formal proof.

The RoboCup Logistics League is a RoboCup competition in a smart factory scenario that has focused on task planning, job scheduling, and multi-agent coordination. The focus on production logistics allowed teams to develop highly competitive strategies, but also meant that some recent developments in the context of smart manufacturing are not reflected in the competition, weakening its relevance over the years. In this paper, we describe the vision for the RoboCup Smart Manufacturing League, a new competition designed as a larger smart manufacturing scenario, reflecting all the major aspects of a modern factory. It will consist of several tracks that are initially independent but gradually combined into one smart manufacturing scenario. The new tracks will cover industrial robotics challenges such as assembly, human-robot collaboration, and humanoid robotics, but also retain a focus on production logistics. We expect the reenvisioned competition to be more attractive to newcomers and well-tried teams, while also shifting the focus to current and future challenges of industrial robotics.

Only-knowing was originally introduced by Levesque to capture the beliefs of an agent in the sense that its knowledge base is all the agent knows. When a knowledge base contains defaults Levesque also showed an exact correspondence between only-knowing and autoepistemic logic. Later these results were extended by Lakemeyer and Levesque to also capture a variant of autoepistemic logic proposed by Konolige and Reiter's default logic. One of the benefits of such an approach is that various nonmonotonic formalisms can be compared within a single monotonic logic leading, among other things, to the first axiom system for default logic. In this paper, we will bring another large class of nonmonotonic systems, which were first studied by McDermott and Doyle, into the only-knowing fold. Among other things, we will provide the first possible-world semantics for such systems, providing a new perspective on the nature of modal approaches to nonmonotonic reasoning.

The situation calculus is a popular formalism for reasoning about actions and change. Since the language is first-order, reasoning in the situation calculus is undecidable in general. An important question then is how to weaken reasoning in a principled way to guarantee decidability. Existing approaches either drastically limit the representation of the action theory or neglect important aspects such as sensing. In this paper we propose a model of limited belief for the epistemic situation calculus, which allows very expressive knowledge bases and handles both physical and sensing actions. The model builds on an existing approach to limited belief in the static case. We show that the resulting form of limited reasoning is sound with respect to the original epistemic situation calculus and eventually complete for a large class of formulas.

Industries are on the brink of widely accepting a new paradigm for organizing production by having autonomous robots manage in-factory processes. This transition from static process chains towards more automation and autonomy poses new challenges in terms of, e.g., efficiency of production processes. The RoboCup Logistics League (RCLL) has been proposed as a realistic testbed to study the above mentioned problem at a manageable scale. In RCLL, teams of robots manage and optimize the material flow according to dynamic orders in a simplified factory environment. In particular, robots have to transport workpieces among several machines scattered around the factory shop floor. Each machine performs a specific processing step, orders that denote the products which must be assembled with these operations are posted at run-time and require quick planning and scheduling. Orders also come with a delivery time window, therefore introducing a temporal component into the problem. Though there exist successful heuristic approaches to solve the underlying planning and scheduling problems, a disadvantage of these methods is that they provide no guarantees about the quality of the solution. A promising solution to this problem is offered by the recently emerging field of Optimization Modulo Theories (OMT), where Satisfiability Modulo Theories (SMT) solving is extended with optimization functionalities. In this paper, we present an approach that combines bounded model checking and optimization to generate optimal controllers for multi-robot systems. In particular, using the RoboCup Logistics League as a testbed, we build formal models for robot motions, production processes, and for order schedules, deadlines and rewards. We then encode the synthesis problem as a linear mixed-integer problem and employ Optimization Modulo Theories to synthesize controllers with optimality guarantees.

Hence, at a coarse-grained level of abstraction, KB-Ss can be characterized in terms of two components: (1) a knowledge base, encoding the knowledge embodied by the system, and (2) a reasoning engine, which is able to query the knowledge base, infer or acquire knowledge from external sources, and add new knowledge to the knowledge base. A knowledge-level account of a KBS (that is, a competencecentered, implementation-independent description of a system), such as Clancey's (1985) analysis of first-generation rule-based systems, focuses on the task-centered competence of the system; that is, it addresses issues such as what kind of problems the KBS is designed to tackle, what reasoning methods it uses, and what knowledge it requires. In contrast with task-centered analyses, Levesque and Lakemeyer focus on the competence of the knowledge base rather than that of the whole system. Hence, their notion of competence is a task-independent one: It is the "abstract state of knowledge" (p. This is an interesting assumption, which the "proceduralists" in the AI community might object to: According to the procedural viewpoint of knowledge representation, the knowledge modeled in an application, its representation, and the associated knowledge-retrieval mechanisms have to be engineered as As a result, they would argue, it is not possible to discuss the knowledge of a system independently of the task context in which the system is meant to operate.

KI is the main German national conference in AI, but it addresses an international audience by adopting English as the conference language and having the proceedings published in the Springer Lecture Notes in AI series (Jarke, Koehler, and Lakemeyer 2002). Of the 58 submissions from 17 countries, 20 were selected for presentation by the program committee, chaired by Jana Koehler, IBM Zurich, and Gerhard Lakemeyer, RWTH Aachen. Matthias Jarke, RWTH Aachen, was the general chair. The papers covered a broad range of areas, including multiagent systems, machine learning, natural language processing, constraint reasoning, knowledge representation, planning, and temporal reasoning. The paper by Franz Baader and Anni-Yasmin Turhan, TU Dresden, "On the Problem of Computing Small Representations of Least Common Subsumers," received the best paper award, sponsored by Springer-Verlag.

There are however, a variety of different approaches that claim to capture the true nature of this concept. One reason for this diversity lies in the fact that abductive reasoning occurs in a multitude of contexts. It concerns cases that cover the simplest selection of already existing hypotheses to the generation of new concepts in science. It also concerns cases where the observation is puzzling because it is novel versus cases in which the surprise concerns an anomalous observation. For example, if we wake up, and the lawn is wet, we might explain this observation by assuming that it must have rained or that the sprinklers have been on.

A principled way to study limited forms of reasoning for expressive knowledge bases is to specify the reasoning problem within a suitable logic of limited belief. Ideally such a logic comes equipped with a perspicuous semantics, which provides insights into the nature of the belief model and facilitates the study of the reasoning problem. While a number of such logics were proposed in the past, none of them is able to deal with function symbols except perhaps for the special case of logical constants. In this paper we propose a logic of limited belief with arbitrary function symbols. Among other things, we demonstrate that this form of limited belief has desirable properties such as eventual completeness for a large class of formulas and that it serves as a specification of a form of decidable reasoning for very expressive knowledge bases.

Only knowing captures the intuitive notion that the beliefs of an agent are precisely those that follow from its knowledge base. It has previously been shown to be useful in characterizing knowledge-based reasoners, especially in a quantified setting. While this allows us to reason about incomplete knowledge in the sense of not knowing whether a formula is true or not, there are many applications where one would like to reason about the degree of belief in a formula. In this work, we propose a new general first-order account of probability and only knowing that admits knowledge bases with incomplete and probabilistic specifications. Beliefs and non-beliefs are then shown to emerge as a direct logical consequence of the sentences of the knowledge base at a corresponding level of specificity.