ICLP on Sunday, July 18th

09:00‑10:00 Technical Communications - III
Chair: Agostino Dovier
Location: AT LT3
09:00 Kim Bauters, Jeroen Janssen, Steven Schockaert, Dirk Vermeir and Martine De Cock
Communicating Answer Set Programs

Answer set programming is a form of declarative programming that has proven very successful in succinctly formulating and solving complex problems. Although some mechanisms for representing and reasoning with the combined answer set programs of multiple agents have already been proposed, the actual gain in expressivity when adding communication has not been studied. We show that allowing simple programs to talk to each other results in the same expressivity as adding negation-as-failure. Furthermore, we show that the ability to focus on one program in a network of simple programs results in the same expressivity as adding disjunction in the head of the rules.

09:12 Timur Fayruzov, Jeroen Janssen, Martine De Cock, Chris Cornelis and Dirk Vermeir
Efficient solving of time-dependent answer set programs

In many application domains of answer set programming the grounding size of a program directly depends on one or more parameters. As the grounding size directly influences the computational effort required for finding answer sets, a formal study of the conditions under which this grounding can be reduced is vital for making answer set programming a feasible modelling tool in these domains. In this paper we study a specific class of programs whose grounding size depends on a time parameter, viz. Markovian programs. We show how the solving time of these programs can significantly be reduced by successively finding answer sets of parts of the grounded program, instead of directly solving the whole program. A practical algorithm is introduced, which allows more efficient solvers to be built, paving the way for answer set programming as a practical modelling tool in these domains.

09:24 Marcello Balduccini
Learning Domain-Specific Heuristics for Answer Set Solvers

In spite of the recent improvements in the performance of Answer Set Programming (ASP) solvers, when the search space is sufficiently large, it is still possible for the search algorithm to mistakenly focus on areas of the search space that contain no solutions or very few. When that happens, performance degrades substantially, even to the point that the solver may need to be terminated before returning an answer. This prospect is a concern when one is considering using such a solver in an industrial setting, where users typically expect consistent performance. To overcome this problem, in this paper we propose a technique that allows learning domain-specific heuristics for ASP solvers. The learning is done off-line, on representative instances from the target domain, and the learned heuristics are then used for choice-point selection. In our experiments, the introduction of domain-specific heuristics improved performance on hard instances by up to almost $3$ orders of magnitude, nearly completely eliminating the cases in which the solver had to be terminated because the wait for an answer had become unacceptable.

09:36 Tomi Janhunen
Sampler Programs: The Stable Model Semantics Abstract Constraint Programs Revisited

Abstract constraint atoms provide a general framework for the study of aggregates utilized in answer set programming. Such primitives suitably increase the expressive power of rules and enable the more concise representation of various domains as answer set programs. However, it is non-trivial to generalize the stable model semantics for programs involving arbitrary abstract constraint atoms. For instance, a nondeterministic variant of the immediate consequence operator is needed, or the definition of stable models cannot be stated directly using primitives of logic programs. In this paper, we propose sampler programs as a relaxation of abstract constraint programs that better lend themselves to the program transformation involved in the definition of stable models. Consequently, the declarative nature of stable models can be restored for sampler programs and the definition also covers abstract constraint programs when decomposed into sampler programs. Moreover, we study the relationships of the classes of programs involved and provide a characterization in terms of abstract but essentially deterministic computations. This result indicates that all nondeterminism related with abstract constraint atoms can be resolved at the level of program reduct when sampler programs are used as the intermediate representation.

09:48 Johannes Oetsch, Joerg Puehrer and Hans Tompits
Methods and Methodologies for Developing Answer-Set Programs---Project Description

Answer-set programming (ASP) is a well-known formalism for declarative problem solving, witnessed by a continuously increasing number of diverse applications. However, one of the main challenges for a wider acceptance of ASP is the need of tools, methods, and methodologies that support the actual programming process. In this paper, we review the main goals of a project, funded by the Austrian Science Fund (FWF), which aims at addressing this aspect in a systematic manner. The project is planned for a duration of three years and started in September 2009. Generally, the focus of research will be on methodologies for systematic program development, program testing, and debugging. In particular, in working on these areas, special emphasis shall be given to modular programming concepts and to the ability of the developed techniques to respect the declarative nature of ASP. To support a sufficient level of applicability, we plan to offer solutions not only for the core language of ASP but also for important extensions thereof that are commonly used and realised in various answer-set solvers. The methods resulting from the project should be incorporated in an integrated development environment for ASP that combines straightforward as well as advanced techniques realising a convenient tool for developing answer-set programs.

10:30‑12:30 Knowledge Representation and Reasoning
Chair: Ilkka Niemela
Location: AT LT3
10:30 Yisong Wang, Jia-Huai You, Li-Yan Yuan and Yi-Dong Shen
Loop Formulas for Description Logic Programs

Description Logic Programs (dl-programs) proposed by Eiter et al. is an integration of answer set programming with description logics for semantic web. In the paper, we generalize the notions of completion and loop formulas of logic programs to description logic programs and show that the weak and strong answer set semantics can be precisely captured by the models of the completion together with the corresponding weak and strong loop formulas. Based on the completion and a general loop formulas, we propose a new semantics for dl-programs which is free of circular justification. Some properties of the semantics are explored as well.

11:00 Martin Slota and João Leite
Towards Closed World Reasoning in Dynamic Open Worlds

The need for integration of ontologies with nonmonotonic rules has been gaining importance in a number of areas, such as the Semantic Web. A number of researchers addressed this problem by proposing a unified semantics for hybrid knowledge bases composed of both an ontology (expressed in a fragment of first-order logic) and nonmonotonic rules. These semantics have matured over the years, but only provide solutions for the static case when knowledge does not need to evolve.

In this paper we take a first step towards addressing the dynamics of hybrid knowledge bases. We focus on knowledge updates and, considering the state of the art of belief update, ontology update and rule update, we show that current solutions are only partial and difficult to combine. Then we extend the existing work on ABox updates with rules, provide a semantics for such evolving hybrid knowledge bases and study its basic properties.

To the best of our knowledge, this is the first time that an update operator has been proposed for hybrid knowledge bases.

11:30 James Delgrande
A Program-Level Approach to Revising Logic Programs under the Answer Set Semantics

We present an approach to the \emph{revision} of logic programs under the answer set semantics. For logic programs $P$ and $Q$, the goal is to determine the answer sets that correspond to the revision of $P$ by $Q$, denoted $P * Q$. A fundamental principle of classical (AGM) revision, and one that guides the approach here, is the \emph{success postulate}. In AGM revision, this postulate stipulates that $A \in K \revise A$. By analogy with the success postulate, for programs $P$ and $Q$, this means that the answer sets of $Q$ will in some sense be contained in those of $P * Q$. The essential idea is that for $P * Q$, a three-valued answer set for $Q$, consisting of positive and negative atoms, is first determined. The positive atoms constitute a regular answer set, while the negated atoms make up a minimal set of naf atoms needed to produce the answer set from $Q$. These atoms are propagated to the program $P$, along with those rules of $Q$ that are not \emph{decided} by these atoms. The approach differs from work in \emph{update logic programs} in two main respects: first, we satisfy the success postulate; second, for the preference implicit in a revision $P * Q$, the program $P$ as a whole takes precedence over $Q$, unlike update logic programs, where the preference is at the level of individual rules. We show that a selection of the AGM postulates are satisfied, as are the postulates that have been proposed for update logic programs. Complexity results are discussed, as is an implementation of the approach.

12:00 Ping Hou, Broes De Cat and Marc Denecker
FO(FD): Extending classical logic with rule-based fixpoint definitions

We introduce the fixpoint definitions, which is a rule-based reformulation of fixpoint constructs. We define the logic FO(FD), an extension of classical logic with fixpoint definitions. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms . We investigate the satisfiability problem of FO(FD) by first reducing FO(FD) to difference logic and then using SAT solvers for difference logic. We evaluate the SMT solvers in the computation of models of FO(FD) theories using these reductions and a selection of experiments. To this end, we provide potential applications of FO(FD).

14:00‑15:00 FLoC Keynote Talk: Deepak Kapur
Location: George Square Lecture Theatre
14:00 Deepak Kapur (University of New Mexico)
Induction, Invariants, and Abstraction

Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated.

15:30‑17:00 CHR and CLP
Chair: Terrance Swift
Location: AT LT3
15:30 Hariolf Betz, Frank Raiser and Thom Fruehwirth
A Complete and Terminating Execution Model for Constraint Handling Rules

We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics~$\obang$, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.

16:00 Maurizio Gabbrielli, Jacopo Mauro, Maria Chiara Meo and Jon Sneyers
Decidability properties for fragments of CHR

In this paper we study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which do not allow function symbols (of arity > 0). Both languages allow to use the = built-in the the body of rules, thus are built on a host language that support unification, however they impose one further restriction each. The first CHR dialect allows range restricted rules only, that is, does not allow to use in the body of a rule a variable which do not appear in the head. We show that in this case the existence of a divergent termination is decidable. The second dialect instead limit to one the number of atoms in the head of rules. We prove that, for this language, the existence of a terminating computation is decidable. It is worth noting that while these results show that both these dialects are strictly less expressive than Turing Machines, the language (without function symbols) obtained by removing these restriction is still Turing complete.

16:30 Mario Rodríguez-Artalejo and Carlos A. Romero-Díaz
A Declarative Semantics for CLP with Qualification and Proximity

Uncertainty in Logic Programming has been investigated during the last decades, dealing with various extensions of the classical LP paradigm and different applications. Existing proposals rely on different techniques, such as clause annotations based on uncertain truth values, qualification values as a generalization of uncertain truth values, and unification based on proximity relations. On the other hand, the CLP scheme has established itself as a powerful extension of LP that supports efficient computation over specialized domains while keeping a clean declarative semantics. In this paper we propose a new scheme SQCLP designed as an extension of CLP that supports qualification values and proximity relations. We show that several previous proposals can be viewed as particular cases of the new scheme, obtained by partial instantiation. We present a declarative semantics for SQCLP that is based on observables, providing fixpoint and proof-theoretical characterizations of least program models as well as an implementation-independent notion of goal solutions.