Methods for Modalities 1
Invited Talks
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.

Methods for Modalities
Contact address

Henry Chinaski Productions 1999