| | Sessions
take place in auditorium 4 unless otherwise indicated.*Chair:*
Peter Stuckey
09:00- | 10:00
| Stefan Decker, Stanford U, USA Invited
talk: **Logic databases on the semantic web: Challenges and
opportunities** Until
now, the Web has mainly designed for direct human
consumption. The next step in the evolution, dubbed the "Semantic Web",
aims at machine-processable information, enabling intelligent services such
as information brokers, search agents, information filters, and direct B2B
communication, which offers greater functionality and interoperability than
the current stand-alone services.
The development of the Semantic Web
creates opportunities and challenges for logic databases. Languages need to
be developed which allow us to specify data transformations for various
data models. Efficient query and inference techniques have to be developed.
Technologies developed by the Logic Programming and Deductive Database
Community can help to built the Semantic Web by overcoming these
problems. |
10:00- | 10:30
| François Bry, U Munich, Germany Sebastian
Schaffert, U Munich, Germany
**Towards
a declarative query and transformation language for XML and
semistructured data: Simulation unification** The
growing importance of XML as a data interchange standard
demands languages for data querying and transformation. Since the mid 90es,
several such languages have been proposed that are inspired from functional
languages (such as XSLT) and/or database query languages (such as XQuery).
This paper addresses applying logic programming concepts and techniques to
designing a declarative, rule-based query and transformation language for
XML and semistructured data.
The paper first introduces issues
specific to XML and semistructured data such as the necessity of flexible
"query terms" and of "construct terms". Then, it is argued
that logic programming concepts are particularly appropriate for a
declarative query and transformation language for XML and semistructured
data. Finally, a new form of unification, called "simulation unification", is
proposed for
answering "query terms", and it
is illustrated on examples. |
*Chair:*
Michael Maher
11:00- | 11:30
| Brigitte Pientka, Carnegie Mellon U, USA
**A
proof-theoretic foundation for tabled higher-order logic
programming** Higher-order
logic programming languages such as *Elf* extend first-order logic
programming in two ways:
first-order terms are replaced with (dependently) typed *λ*-terms
and the body of clauses may
contain implication and universal quantification. In this paper, we
describe *tabled higher-order logic programming* where some
redundant computation is eliminated by memoizing sub-computation and
re-using its result later. This work extends Tamaki and Sato's search
strategy based on memoization to the higher-order setting. We give a
proof-theoretic characterization of tabling based on uniform proofs and
prove soundness of the resulting interpreter. Based on it, we have
implemented a prototype of a tabled logic programming interpreter for *Elf*. |
11:30- | 12:00
| Sorin Craciunescu, INRIA Rocquencourt, France
**Proving
the equivalence of CLP programs** This
paper presents two proof systems for the equivalence of
programs. The language concerned is CLP to which the universal quantifier
is added (CLP∀). Both systems are
based on first order classical logic.
The first uses an induction rule
and allows one to prove that the set of finite successes of a program is
included in another program's corresponding set. The second uses a
coinduction rule for proving the inclusion of the sets of infinite
successes which contain the finite successes.
Finally we show that the
proof systems are equivalent under some natural conditions. |
12:00- | 12:30
| Paola Bruscoli, Dresden U of Techn., Germany
**A
purely logical account of sequentiality in proof search** A
strict correspondence between the proof-search space of a
logical formal system and computations in a simple process algebra is
established. Sequential composition in the process algebra corresponds to a
logical relation in the the formal system - in the
sense our approach is purely logical, no axioms or encodings are involved.
The process algebra is a minimal restriction of CCS to parallel and
sequential composition; the logical system is a minimal extension of
multiplicative linear logic. This way we get the first purely logical
account of sequentiality in proof search. Since we restrict attention to a
small meaningful fragment, which is then of very broad interest, our
techniques should become a common basis for several possible extensions. In
particular, we argue about this work being the first step in a two-step
research for capturing most of CCS in a purely logical fashion. |
*Chair:*
Mirek Truszczynski
16:00- | 16:30
| Katsumi Inoue, Kobe U, Japan Chiaki
Sakama, Wakayama U, Japan
**Disjunctive
explanations** Abductive
logic programming has been widely used to declaratively
specify a variety of problems in AI including updates in data and knowledge
bases, belief revision, diagnosis, causal theory, and default reasoning.
One of the most significant issues in abductive logic programming is to
develop a reasonable method for *knowledge assimilation*,
which incorporates obtained explanations into the current knowledge base.
This paper offers a solution to this problem by considering *disjunctive
explanations* whenever
multiple explanations exist. Disjunctive explanations are then to be
assimilated into the knowledge base so that the assimilated program
preserves all and only minimal answer sets from the collection of all
possible updated programs. We describe a new form of abductive logic
programming which deals with disjunctive explanations in the framework of
*extended abduction*. The proposed framework can be well
applied to view updates in disjunctive databases. |
*Room:*
Nyhavn
Joint
with TABLEAUX
*Room:*
Restaurant Luftkastellet 20:30- | 22:00
| Veronica Dahl, Simon Fraser U, Canada Banquet
speaker: **Title TBA** |
| |