|
- Monday, September 22, 9:30-10:45
- Maarten Marx,
Variable Free Reasoning on Finite Trees
Reasoning about finite ordered trees is becoming very important with
the advent of the new data storage format XML. XPath is the most
widely used language to retrieve data from XML documents.
We show the close connection between XPath and various well
investigated variable free formalisms interpreted on trees: Kleene
algebras with Tests,
Propositional Dynamic logic, since/until
temporal logic.
We present an extension of XPath which can express all first order
definable queries over ordered trees.
We give a linear time algorithm for query evaluation for a language
which extends XPath with all regular expressions and tests over the
four basic axes.
We give an EXPTIME decision algorithm which can be used to decide
equivalence of a large number of XPath expressions given a set of
constraints (eg, an XML Schema Definition or a Document
Type Definition (DTD).
- Monday, September 22, 14:30-15:45
- Stephan Merz,
The automata-theoretic framework for model checking revisited
The automata-theoretic approach to temporal logic model checking has
been developed in the seminal papers of Vardi, Wolper, and others, but
continues to evolve. This talk will give an introduction to some of the
more recent work based on alternating automata and games that are
starting to find their way into implementations.
- Monday, September 22, 17:45-19:00
- Claude Kirchner,
An Introduction to Deduction Modulo
This talk will present the general idea of deduction modulo with
motivations from proof presentation and proof search.
We will see how the general concepts can be used for inductive proofs
by rewriting and how a proof search method can be given that
generalizes first as well as higher-order resolution.
- Tuesday, September 23, 9:30-10:45
- Stephane Demri,
(Modal) Logics for Semistructured Data (bis)
Many query languages for semistructured data have been designed in the last
few years, some of them having a clear modal flavor. In this talk,
we present different reasoning tasks for semistructured data that can be
naturally expressed by modal languages. We shall emphasize the peculiarities of
the different approaches from the literature and how they
compare with works without an explicit modal perspective. The variety of modal logics
dedicated to semistructured data and their apparent
unstructured development are mainly due to the numerous
ways semistructured data can be abstracted (graphs, trees, ...) and to the various types
of constraints of interest (path constraints, type constraints, numerical queries, ...)
expressed for instance by regular expressions and Presburger constraints.
- Tuesday, September 23, 14:30-15:45
- Carsten Lutz,
Expressivity and Complexity of Description Logics with Concrete Domains
In standard description logics (DLs) such as ALC, it is not possible
to capture `concrete qualities'' of real-world entities such as their
weight, height, duration, and spatial extension. To cure this defect,
concrete domains have been proposed as an extension to standard DLs.
Driven by the usual trade-off between expressive power and computational
complexity, in this talk we survey the various variants of concrete
domains that have been considered in the literature. It turns out that
description logics with concrete domains are rather sensitive w.r.t.
extensions of the formalism, as even seemingly simple modifications
often result in a leap to higher complexity classes, or even to
undecidability.
- Tuesday, September 23, 17.45-19.00
- Ralf Moeller,
The Ins and Outs of Racer
Description logic (DL) systems are now used in many
application and research projects. The architecture of full-fledged DL
systems such as Racer is oriented towards large knowledge bases and
various kinds of access patterns. The talk presents the architecture of
the Racer system and its inference services. Main ideas of optimization
techniques for answering important kinds of queries will be sketched.
Meanwhile many experiences exist with applications of Racer. However,
at the current state of the art, DL inference technology is brought to
its limit by many users. The talk will summarize the requirements of
the projects Racer has been used for, and will demonstrate some new
features that allow for new ways to use DL systems in various projects.
In particular, the talk will illustrate for what set of requirements
current DL systems can successfully be used and for what set of
requirements serious difficulties can be expected due the nature of the
architecture of current systems.
|
|
