 | |
All
sessions take place in auditorium 4.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. |
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. |
| 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 |
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. |
|