ABSTRACT. Modular systems offer a language-independent declarative framework in which modules from different languages are combined to describe a conceptually and/or computationally complex problem. The original semantics developed to combine modules in a modular system is a model-theoretical semantics with close ties to relational algebraic operations.

In this paper, we introduce a new semantics for modular systems, called supported model semantics, that extends the original model-theoretic semantics of modular systems and captures non-monotonic reasoning on the level of modular system (rather than the level of individual modules). Moreover, we also use supported model semantics for modular systems to compare the expressiveness of modular systems with that of heterogeneous non-monotonic multi-context systems [BE'07]. We show that, under very few conditions, all multi-context systems can be translated into equivalent modular systems. Our result is true for both major semantics of multi-context systems, i.e., the equilibrium semantics and the grounded equilibrium semantics. Thus, we show that modular systems under supported model semantics generalize multi-context systems under either of its major semantics.

ABSTRACT. Strong equivalence of logic programs is an important concept in the theory of answer set programming. Equilibrium logic was used to show that propositional formulas are strongly equivalent if and only if they are equivalent in the logic of here-and-there. We extend equilibrium logic to formulas with infinitely long conjunctions and disjunctions, define and axiomatize an infinitary counterpart of the logic of here-and-there, and show that the theorem on strong equivalence holds in the infinitary case as well.

ABSTRACT. In this paper we present a new version of the language of Epistemic Specifications. The goal is to simplify and improve the intuitive and formal semantics. We describe an algorithm for computing solutions of programs written in this new version of the language. The new semantics is illustrated by a number of examples, including an Epistemic Specifications-based framework for conformant planning.

ABSTRACT. An epistemic logic program is a program written in the language of Epistemic Specifications, an extension of the language of answer set programming (ASP) that allows for introspective reasoning through the use of modal operators K and M. The language of Epistemic Specifications was introduced by Gelfond in the early 1990s after observing the need for a more powerful form of introspective reasoning than that offered by ASP alone. The semantics of an epistemic logic program was given in terms of its world view--a collection of sets of literals (belief sets), analogous to the answer sets of an ASP program. In 2011, Gelfond proposed a change to the semantics in a preliminary attempt to avoid certain unintended world views. Gelfond, Kahl, Watson, and Zhang continued this work in the hopes of finding a semantics that was satisfactory with respect to intuition and modeling of problems for which the added power of Epistemic Specifications showed promise.

Concurrent with this latter work was an effort by Balai, Gelfond, and Zhang to enhance ASP by providing a framework for specifying sorts for the parameters of predicates in a language they called SPARC. This promoted better program design, helped to eliminate certain common errors (e.g., misspellings), and encouraged development of rules specific to a particular domain without the concern for rule safety that has been associated with variable terms by popular ASP solvers (e.g., clingo, DLV).

In this paper, we combine these recent efforts by providing within the language of Epistemic Specifications a framework for specifying predicate parameter domains. We call a program written in this new language an epistemic logic program with sorts (ELPS). In addition to the benefits a sorted signature provides to the programmer, it also allows for a straightforward algorithm for computing world views. We describe such an algorithm--one that can take advantage of existing state-of-the-art ASP solvers--and give a synopsis of test results from our implementation. We conclude with a discussion of related work and a brief summary.

ABSTRACT. Many scenarios in Answer Set Programming (ASP) deal with dynamic systems over (potentially infinite) linear time. Temporal Equilibrium Logic (TEL) is a formalism that allows defining the idea of "temporal stable model" not only for dynamic domains in ASP, but aso for any arbitrary theory in the syntax of Linear-Time Temporal Logic (LTL). In the past, several tools for computing temporal stable models have been built using well-established LTL and automata techniques. These tools displayed the set of temporal stable models of a given theory as a Büchi-automaton and, in many cases, it was also possible to capture such a set by the LTL-models of a given temporal formula. The fundamental theoretical question of whether this was a general property or not remained open, since it is well-known that, in general, Büchi-automata are more expressive than LTL. In this paper we show that, indeed, the set of temporal stable models of any arbitrary temporal theory can be succinctly captured as the LTL models of a given temporal formula.

ABSTRACT. Action language BC provides an elegant way of formalizing robotic domains which need to be expressed using default logic as well as indirect and recursive action effects. However, generating plans efficiently for large domains using BC can be challenging, even when state-of-the-art answer set solvers are used. Since a number of task planning domains in mobile robotics can be easily broken up hierarchically using macro-actions, we investigate the computational gains achieved by planning over a hierarchical abstraction of the domain. Each layer of abstraction is described independently using BC, and we plan independently over each description, resolving macro-actions as we go down the hierarchy. We present a case study where at least an order of magnitude speedup was achieved in a robot mail collection task by using hierarchical domain abstractions.

ABSTRACT. Recently, action language BC, which combines the attractive features of action languages B and C+, was proposed. While BC allows Prolog-style recursive definitions that are not available in C+, it is less expressive than C+ in other ways, such as inability to express non-Boolean and non-exogenous actions. We propose a new action language called BC+, which encompasses all the features of BC and the definite fragment of C+. The syntax of BC+ is identical to the syntax of C+ allowing arbitrary propositional formulas in the causal laws, but its semantics is defined in terms of propositional formulas under the stable model semantics instead of nonmonotonic causal theories. This approach allows many useful ASP constructs, such as choice rules and aggregates, to be directly used in language BC+, and exploits computational methods available in ASP solvers. 

ABSTRACT. In recent work, we defined Resource-Based Answer Set Semantics, which is an extension to traditional answer set semantics stemming from the study of its relationship with linear logic. In this setting there are no inconsistent programs, and constraints are defined "per se" in a separate layer. In this paper, we propose a query-answering procedure reminiscent of Prolog for answer set programs under this extended semantics.

ABSTRACT. Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such structural properties is non-obvious and can be challenging indeed. In this paper, we take a number of acyclicity properties into consideration and investigate various 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. We study the compactness of encodings and the resulting computational performance on benchmarks involving acyclic or tree structures.

ABSTRACT. Problems from the area of graph theory always served as fruitful benchmarks in order to explore the performance of Answer Set Programming (ASP) systems. A relatively new branch in graph theory is concerned with so-called secure sets. It is known that verifying whether a set is secure in a graph is already co-NP-hard. The problem of enumerating all secure sets thus is challenging for ASP and its systems. In particular, encodings for this problem seem to require disjunction and also recursive aggregates. In this paper, we provide such encodings and analyze their performance using the Clingo system.

ABSTRACT. In this paper we introduce asprin [1], a general, flexible, and extensible framework for handling preferences among the stable models of a logic program. We show how complex preference relations can be specified through user-defined preference types and their arguments. We describe how preference specifications are handled internally by so-called preference programs which are used for dominance testing. We also give algorithms for computing one, or all, optimal stable models of a logic program. Notably, the algorithms depend on the complexity of the dominance tests and make use of incremental answer set solving technology.

[1] asprin stands for ``{AS}P for {Pr}eference handl{in}g''.

ABSTRACT. Optimization problems in Answer Set Programming (ASP) are usually modeled by means of programs with weak constraints. These programs can be handled by algorithms for solving Maximum Satisfiability (MaxSAT) problems, if properly ported to the ASP framework. This paper reports on the implementation of several of these algorithms in the ASP solver WASP, whose empirical analysis highlights pros and cons of different strategies for computing optimal answer sets.

ABSTRACT. Broad application of answer set programming (ASP) for declarative problem solving requires the development of tools supporting the coding process. Program debugging is one of the crucial activities within this process. Modern ASP debugging approaches allow efficient computation of possible explanations of a fault. However, even for a small program a debugger might return a large number of possible explanations and selection of the correct one must be done manually.

In this paper we present an interactive query-based ASP debugging method which extends previous approaches and finds a preferred explanation by means of observations. The system automatically generates a sequence of queries to a programmer asking whether a set of ground atoms must be true in all (cautiously) or some (bravely) answer sets of the program. Since some queries can be more informative than the others, we discuss query selection strategies which, given user's preferences for an explanation, can find the best query. That is, the query an answer of which reduces the overall number of queries required for the identification of a preferred explanation.

ABSTRACT. In this paper the applicability of the MapReduce framework for parallel computation for monadic logic programs is studied. In monadic programs all predicates are of arity one. Two different approaches are suggested: the first is based on parallelizing on constants, the second parallelizes on predicates. In each case, a method is provided that makes use of MapReduce and calls standard ASP solvers as back-ends via an abstract API. For each method, we provide a theoretical analysis of its computational impact.