The advance of Internet and Sensor technology has brought about new challenges evoked by the emergence of continuous data streams. While existing data-stream management systems allow for high-throughput stream processing, they lack complex reasoning capacities. We address this shortcoming and elaborate upon an approach to knowledge-intense stream reasoning based on Answer Set Programming (ASP). The emphasis thus shifts from rapid data processing to complex reasoning. To accommodate this in ASP, we develop new techniques that allow us to formulate problem encodings dealing with emerging as well as expiring data in a seamless way. We thus propose novel language constructs and modeling techniques for specifying and reasoning with time-decaying logic programs.

Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such properties is non-obvious and can be challenging indeed. In this paper, we take acyclicity properties into consideration and investigate logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic, and linear programming.

Automated storage and retrieval systems are principal components of modern production and warehouse facilities. In particular, automated guided vehicles nowadays substitute human-operated pallet trucks in transporting production materials between storage locations and assembly stations. While low-level control systems take care of navigating such driverless vehicles along programmed routes and avoid collisions even under unforeseen circumstances, in the common case of multiple vehicles sharing the same operation area, the problem remains how to set up routes such that a collection of transport tasks is accomplished most effectively. We address this prevalent problem in the context of car assembly at Mercedes-Benz Ludwigsfelde GmbH, a large-scale producer of commercial vehicles, where routes for automated guided vehicles used in the production process have traditionally been hand-coded by human engineers. Such ad-hoc methods may suffice as long as a running production process remains in place, while any change in the factory layout or production targets necessitates tedious manual reconfiguration, not to mention the missing portability between different production plants. Unlike this, we propose a declarative approach based on Answer Set Programming to optimize the routes taken by automated guided vehicles for accomplishing transport tasks. The advantages include a transparent and executable problem formalization, provable optimality of routes relative to objective criteria, as well as elaboration tolerance towards particular factory layouts and production targets. Moreover, we demonstrate that our approach is efficient enough to deal with the transport tasks evolving in realistic production processes at the car factory of Mercedes-Benz Ludwigsfelde GmbH.

Answer Set Programming (ASP) is a well-known paradigm of declarative programming with roots in logic programming and non-monotonic reasoning. Similar to other closely related problem-solving technologies, such as SAT/SMT, QBF, Planning and Scheduling, advancements in ASP solving are assessed in competition events. In this paper, we report about the design and results of the Sixth ASP Competition, which was jointly organized by the University of Calabria (Italy), Aalto University (Finland), and the University of Genoa (Italy), in affiliation with the 13th International Conference on Logic Programming and Non-Monotonic Reasoning. This edition maintained some of the design decisions introduced in 2014, e.g., the conception of sub-tracks, the scoring scheme, and the adherence to a fixed modeling language in order to push the adoption of the ASP-Core-2 standard. On the other hand, it featured also some novelties, like a benchmark selection stage classifying instances according to their empirical hardness, and a "Marathon" track where the top-performing systems are given more time for solving hard benchmarks.

The goal of this article is threefold. First, we trace the history of the development of answer set solvers, by accounting for more than a dozen of them. Second, we discuss development tools and environments that facilitate the use of answer set programming technology in practical applications. Last, we present the evolution of the answer set programming competitions, prime venues for tracking advances in answer set solving technology.

At first, a problem is expressed as a logic program. ASP's success is largely due to the availability of a rich modeling language (Gebser and Schaub 2016) along with effective systems. Early ASP solvers SModels (Simons, Niemelä, and Soininen 2002) and DLV (Leone et al. 2006) were followed by SAT DLV (Faber, Leone, and Perri 2012) or GrinGo (Gebser ground rules, corresponding to the number of net al. 2011) are based on seminaive database evaluation tuples, over a set of two elements. For more details techniques (Ullman 1988) for avoiding duplicate about complexity of ASP the reader may refer to work during grounding. Grounding is seen as an iterative Dantsin et al. (2001).

Special-purpose propagators speed up solving logic programs by inferring facts that are hard to deduce otherwise. However, implementing special-purpose propagators is a non-trivial task and requires expert knowledge of solvers. This paper proposes a novel approach in logic programming that allows (1) logical specification of both the problem itself and its propagators and (2) automatic incorporation of such propagators into the solving process. We call our proposed language P [ R ] and our solver SAT-to-SAT because it facilitates communication between several SAT solvers. Using our proposal, non-specialists can specify new reasoning methods (propagators) in a declarative fashion and obtain a solver that benefits from both state-of-the-art techniques implemented in SAT solvers as well as problem-specific reasoning methods that depend on the problem's structure. We implement our proposal and show that it outperforms the existing approach that only allows modeling a problem but does not allow modeling the reasoning methods for that problem.

Stream reasoning is the task of continuously deriving conclusions on streaming data. As a research theme, it is targeted by different communities which emphasize different aspects, e.g., throughput vs. expressiveness. This thesis aims to advance the theoretical foundations underlying diverse stream reasoning approaches and to convert obtained insights into a prototypical expressive rule-based reasoning system that is lacking to date.

This paper proposes an alternative definition of elementary loops and extends the notion of proper loops for disjunctive logic programs. Different from normal logic programs, the computational complexities of recognizing elementary loops and proper loops for disjunctive programs are coNP-complete. To address this problem, we introduce weaker versions of both elementary loops and proper loops and provide polynomial time algorithms for identifying them respectively. On the other hand, based on the notion of elementary loops, the class of Head-Elementary-loop-Free (HEF) programs was presented, which can be turned into equivalent normal logic programs by shifting head atoms into bodies. However, the problem of recognizing an HEF program is coNP-complete. Then we present a subclass of HEF programs which generalizes the class of Head-Cycle-Free programs and provide a polynomial time algorithm to identify them. At last, some experiments show that both elementary loops and proper loops could be replaced by their weak versions in practice.

Drescher and Walsh, to satisfiability modulo theories, the key idea is to incorporate 2010). Then, constraint answer sets of the resulting program theory-specific predicates into propositional formulas, can be characterized via Boolean assignments over and extending an ASP solver's decision engine for a atom(Π) body(Π) that do not violate a set of nogoods more high-level proof procedure. A promising approach to imposed by Π. Formally, a Boolean assignment A is a sequence constraint answer set programming (CASP) has been presented (σ