ASPOCP 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

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. In a nutshell, a subset S of vertices is secure if for each X ⊆ S the number of vertices from S that appear in the closed neighborhood of X is not smaller than the number of elements in the closed neighborhood of X not from S (where the closed neighborhood of a set of vertices contains the set itself plus all vertices adjacent to any vertex in that set). 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. 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. Recently, action language $\cal BC$, which combines the attractive features of action languages $\cal B$ and $\cal C$+, was proposed. While $\cal BC$ allows Prolog-style recursive definitions not available in $\cal C$+, it is less expressive than $\cal C$+ in other ways, such as inability to express non-Boolean and non-exogenous actions. We propose a new action language called $\cal BC$+, which encompasses $\cal BC$ and $\cal C$+. The syntax of $\cal BC$+ is essentially identical to the syntax of $\cal C$+, but its semantics is defined in terms of a translation into propositional formulas under the stable model semantics similar to $\cal BC$. By understanding the formulas in causal laws in terms of the stable model semantics, this approach allows many useful ASP constructs, such as choice rules and aggregates, to be directly usable in language $\cal BC$+, and exploits computational methods available in ASP solvers.

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. 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. 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. 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 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. 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. 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.

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. 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.