 | |
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 Room:
Restaurant Luftkastellet | 20:30- | 22:00
| Veronica Dahl, Simon Fraser U, Canada
Banquet
speaker: Title TBA |
|