ICLP on Thursday

Detailed program
Thursday August 1st, 2002
See also the unified by-slot program

All sessions take place in auditorium 4.

Session 13: Stable Models and Answer Sets II

Chair: Katsumi Inoue

09:00-09:30  Piero A. Bonatti, U Milan, Italy
Reasoning with infinite stable models II: Disjunctive programs
The class of finitary normal logic programs - identified recently, by the author - makes it possible to reason effectively with function symbols, recursion, and infinite stable models. These features may lead to a full integration of the standard logic programming paradigm with the answer set programming paradigm. For all finitary programs, ground goals are decidable, while nonground goals are semidecidable. Moreover, the existing engines (that currently accept only much more restricted programs) can be extended to handle finitary programs by replacing their front-ends and keeping their core inference mechanism unchanged. In this paper, the theory of finitary normal programs is extended to disjunctive programs. More precisely, we introduce a suitable generalization of the notion of finitary program and extend all the results of the authors previous work to this class. For this purpose, a consistency result by Fages is extended from normal programs to disjunctive programs. We also correct an error occurring in the previous work.

09:30-10:00  Zbigniew Lonc, Warsaw U of Techn., Poland
Miroslaw Truszczynski, U Kentucky, USA
Computing stable models: Worst-case performance estimates
We study algorithms for computing stable models of propositional logic programs and derive estimates on their worst-case performance that are asymptotically better than the trivial bound of O(m2n), where m is the size of an input program and n is the number of its atoms. For instance, for programs, whose clauses consist of at most two literals (counting the head) we design an algorithm to compute stable models that works in time O(m×1.44225n). We present similar results for several broader classes of programs, as well.

10:00-10:30  Yannis Dimopoulos, U Cyprus
Andreas Sideris, U Cyprus
Towards local search for answer sets
Answer set programming has emerged as a new important paradigm for declarative problem solving. It relies on algorithms that compute the stable models of a logic program, a problem that is, in the worst-case, intractable. Although, local search procedures have been successfully applied to a variety of hard computational problems, the idea of employing such procedures in answer set programming has received very limited attention.
This paper presents several local search algorithms for computing the stable models of a normal logic program. They are all based on the notion of a conflict set, but use it in different ways, resulting in different computational behaviors. The algorithms are inspired from related work in solving propositional satisfiability problems, suitably adapted to the stable model semantics. The paper also discusses how the heuristic equivalence method, that has been proposed in the context of propositional satisfiability, can be used in systematic search procedures that compute the stable models of logic programs.

Session 14: Negation and Extensions

Chair: François Fages

11:00-11:30  Pedro Cabalar, U Corunna, Spain
A rewriting method for well-founded semantics with explicit negation
We present a modification of Brass et al's transformation-based method for the b ottom-up computation of well-founded semantics (WFS), in order to cope with expl icit negation, in the sense of Alferes and Pereira's WFSX semantics. This variat ion consists in the simple addition of two intuitive transformations that guaran tee the satisfaction of the so-called coherence principle: whenever an obj ective literal is founded, its explicit negation must be unfounded. The main con tribution is the proof of soundness and completeness of the resulting method wit h respect to WFSX. Additionally, by a direct inspection on the method, we immedi ately obtain results that help to clarify the comparison between WFSX and regula r WFS when dealing with explicit negation.

11:30-12:00  Grigoris Antoniou, U Bremen, Germany
Michael Maher, Loyola U Chicago, USA
Embedding defeasible logic into logic programs
Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches.
In this paper we establish close links to known semantics of extended logic programs. In particular, we give a translation of a defeasible theory D into a program P(D). We show that under a condition of decisiveness, the defeasible consequences of D correspond exactly to the sceptical conclusions of P(D) under the stable model semantics. Without decisiveness, the result holds only in one direction (all defeasible consequences of D are included in all stable models of P(D)). If we wish a complete embedding for the general case, we need to use the Kunen semantics of P(D), instead.

12:00-12:30  David Pearce, European Commission, Belgium
Vladimir Sarsakov, U Potsdam, Germany
Torsten Schaub, U Potsdam, Germany
Hans Tompits, Vienna U of Techn., Austria
Stefan Woltran, Vienna U of Techn., Austria
A polynomial translation of logic programs with nested expressions into disjunctive logic programs: Preliminary report
Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Previous results show that nested logic programs can be transformed into standard (unnested) disjunctive logic programs in an elementary way, applying the negation-as-failure operator to body literals only. This is of great practical relevance since it allows us to evaluate nested logic programs by means of off-the-shelf disjunctive logic programming systems, like DLV. However, it turns out that this straightforward transformation results in an exponential blow-up in the worst-case, despite the fact that complexity results indicate that there is a polynomial translation among both formalisms. In this paper, we take up this challenge and provide a polynomial translation of logic programs with nested expressions into disjunctive logic programs. Moreover, we show that this translation is modular and (strongly) faithful. We have implemented both the straightforward as well as our advanced transformation; the resulting compiler serves as a front-end to DLV and is publicly available on the Web.

Session 15: Invited Tutorial

14:00-15:30  Abhik Roychoudhury, National U of Singapore
I. V. Ramakrishnan, State U of New York-Stony Brook, USA
Invited tutorial: Program transformations for automated verification

Session 16: Applications II

Chair: Gopal Gupta

16:00-16:30  Henrik Bærbak Christensen, U Aarhus, Denmark
Using logic programming to detect activities in pervasive healthcare
In this experience paper we present a case study in using logic programming in a pervasive computing project in the healthcare domain. An expert system is used to detect healthcare activities in a pervasive hospital environment where positions of people and things are tracked. Based on detected activities an activity-driven computing infrastructure provides computational assistance to healthcare staff on mobile- and pervasive computing equipment. Assistance range from simple activities like fast log-in into the electronic patient medical record system to complex activities like signing for medicine given to specific patients. We describe the role of logic programming in the infrastructure and discuss the benefits and problems of using logic programming in a pervasive context.

16:30-17:00  Tamás Benkö, IQSOFT Intelligent Software, Hungary
Péter Krauth, IQSOFT Intelligent Software, Hungary
Péter Szeredi, IQSOFT Intelligent Software, Hungary
A logic-based system for application integration
The paper introduces the SILK tool-set, a tool-set based on constraint logic programming techniques for the support of application integration. We focus on the Integrator component of SILK, which provides tools and techniques to support the process of model evolution: unification of the models of the information sources and their mapping onto the conceptual models of their user-groups.
We present the basic architecture of SILK and introduce the SILK Knowledge Base, which stores the meta-information describing the information sources. The SILK Knowledge Base can contain both object-oriented and ontology-based descriptions, annotated with constraints. The constraints can be used both for expressing the properties of the objects and for providing mappings between them. We give a brief introduction to SILan, the language for Knowledge Base presentation and maintenance. We describe the implementation status of SILK and give a simple example, which shows how constraints and constraint reasoning techniques can be used to support model evolution.

17:00-17:30  Michael Thielscher, Dresden U of Techn., Germany
Reasoning about actions with CHRs and finite domain constraints
We present a CLP-based approach to reasoning about actions in the presence of incomplete states. Constraints expressing negative and disjunctive state knowledge are processed by a set of special Constraint Handling Rules. In turn, these rules reduce to standard finite domain constraints when handling variable arguments of single state components. Correctness of the approach is proved against the general action theory of the Fluent Calculus. The constraint solver is used as the kernel of a high-level programming language for agents that reason and plan. Experiments have shown that the constraint solver exhibits excellent computational behavior and scales up well.