| | All
sessions take place in auditorium 3.*Chair:*
Christopher Lynch
09:00- | 09:30
| Alfons Geser, NASA Langley, USA
**Loops
of superexponential lengths in one-rule string
rewriting** Loops
are the most frequent cause of non-termination in string
rewriting. In the general case, non-terminating, non-looping string
rewriting systems exist, and the uniform termination problem is
undecidable. For rewriting with only one string rewriting rule, it is
unknown whether non-terminating, non-looping systems exist and whether
uniform termination is decidable. If in the one-rule case, non-termination
is equivalent to the existence of loops, as McNaughton conjectures, then a
decision procedure for the existence of loops also solves the uniform
termination problem. As the existence of loops of bounded lengths is
decidable, the question is raised how long shortest loops may be. We show
that string rewriting rules exist whose shortest loops have
superexponential lengths in the size of the rule. |
09:30- | 10:00
| Elias Tahhan-Bittar, U Simón Bolívar,
Venezuela
**Recursive
derivational length bounds for confluent term rewrite
systems** Let
*F* be a signature and *R* a term rewrite system on ground terms
of *F*. We define the concepts of a context-free
potential redex in a term and of bounded confluent terms. We bound
recursively the lengths of derivations of a bounded confluent term *t* by
a function of the length of derivations of
context-free potential redexes of this term. We define the concept of inner
redex and we apply the recursive bounds that we obtained to prove that,
whenever *R* is a confluent overlay
term rewrite system, the derivational length bound for arbitrary terms is
an iteration of the derivational length bound for inner redexes. |
10:00- | 10:30
| Salvador Lucas, Polytechnic U of Valencia, Spain
**Termination
of (canonical) context-sensitive rewriting** Context-sensitive
rewriting (csr) is a restriction of rewriting
which forbids reductions on selected arguments of functions. A *replacement
map* discriminates, for each symbol of the
signature, the argument positions on which replacements are allowed. If the
replacement restrictions are less restrictive than those expressed by the
so-called *canonical* replacement map, then csr can be used
for computing (infinite) normal forms of terms. Termination of such *canonical* csr is desirable when using csr for these purposes.
Existing transformations for proving termination of csr fulfill a number of
new properties when used for proving termination of canonical
csr. |
*Chair:*
Joachim Niehren
11:00- | 12:00
| Franz
Baader, Dresden U of Techn., Germany Invited
talk: **Engineering of logics for the content-based representation of
information** Storage
and transfer of information as well as interfaces for
accessing this information have undergone a remarkable evolution.
Nevertheless, information systems are still not `intelligent' in the sense
that they `understand' the information they store, manipulate, and present
to their users. A case in point is the world wide web and search engines
allowing to access the vast amount of information available there.
Web-pages are mostly written for human consumption and the mark-up provides
only rendering information for textual and graphical information. Search
engines are usually based on keyword search and often provide a huge number
of answers, many of which are completely irrelevant, whereas some of the
more interesting answers are not found. In contrast, the vision of a
`semantic web' aims for machine-understandable web resources, whose content
can then be comprehended and processed both by automated tools, such as
search engines, and by human users.
The content-based representation
of information requires representation formalisms with a well-defined
formal semantics since otherwise there cannot be a common understanding of
the represented information. This semantics can elegantly be provided by a
translation into an appropriate logic or the use of a logic-based formalism
in the first place. This logical approach has the additional advantage that
logical inferences can then be used to reason about the represented
information, thus detecting inconsistencies and computing implicit
information. However, in this setting there is a fundamental tradeoff
between the expressivity of the representation formalism on the one hand,
and the efficiency of reasoning with this formalism on the other hand.
This motivates the `engineering of logics', i.e., the design of logical
formalisms that are tailored to specific representation tasks. This also
encompasses the formal investigation of the relevant inference problems,
the development of appropriate inferences procedures, and their
implementation, optimization, and empirical evaluation. Another important
topic in this context is the combination of logics and their inference
procedures since a given application my require the use of more than one
specialized logic. The talk will illustrate this approach with the example
of so-called Description Logics and their application as ontology languages
for the semantic web. |
12:00- | 12:30
| Witold Charatonik, MPI Saarbrücken,
Germany Jean-Marc
Talbot, U Lille, France
**Atomic
set constraints with projection** We
investigate a class of set constraints defined as atomic set
constraints augmented with projection. This class subsumes some already
studied classes such as atomic set constraints with left-hand side
projection and INES constraints. All these classes enjoy the nice property
that satisfiability can be tested in cubic time. This is in contrast to
several other classes of set constraints, such as definite set constraints
and positive set constraints, for which satisfiability ranges from
DEXPTIME-complete to NEXPTIME-complete. However, these latter classes allow
set operators such as intersection or union which is not the case for the
class studied here. In the case of atomic set constraints with projection
one might expect that satisfiability remains polynomial. Unfortunately, we
show that that the satisfiability problem for this class is no longer
polynomial, but CoNP-hard. Furthermore, we devise a PSPACE algorithm to
solve this satisfiability problem. |
*Chair:*
Jerzy Marcinkowski
14:00- | 14:30
| Jordi Levy, U Barcelona, Spain Mateu
Villaret, U Girona, Spain
**Currying
second-order unification** The
Curry form of a term, like *f*(*a*,*b*), allows us to write it,
using just a
single binary function symbol, as @(@(*f*,*a*),*b*). Using this
technique we prove that
the signature is not relevant in second-order unification, and conclude
that one binary symbol is enough.
By currying variable applications,
like *X*(*a*), as @(*X*,*a*), we can transform
second-order terms into
first-order terms, but we have to add beta-reduction as a theory. This is
roughly what it is done in explicit unification. We prove that by currying
only constant applications we can reduce second-order unification to
second-order unification with just one binary function symbol. Both
problems are already known to be undecidable, but applying the same idea to
context unification, for which decidability is still unknown, we reduce the
problem to context unification with just one binary function symbol.
We also discuss about the difficulties of applying the same ideas to third
or higher order unification. |
14:30- | 15:00
| Daniel J. Dougherty, Wesleyan U, USA Tomasz
Wierzbicki, U Wroclaw, Poland
**A
decidable variant of higher order matching** A
lambda term is *k*-duplicating if every occurrence of a lambda
abstractor
binds at most *k* variable occurrences. We prove
that the problem of higher order matching where solutions are required to
be *k*-duplicating (but with no constraints on
the problem instance itself) is decidable. We also show that the problem of
higher order matching in the affine lambda calculus (where both the problem
instance and the solutions are constrained to be 1-duplicating) is in NP,
generalizing de Groote's result for the linear
lambda calculus. |
15:00- | 15:30
| Franz Baader, Dresden U of Techn., Germany Cesare
Tinelli, U Iowa, USA
**Combining
decision procedures for positive theories sharing
constructors** This
paper addresses the following combination problem: given two
equational theories *E*_{1} and *E*_{2} whose
positive theories are
decidable, how can one obtain a decision procedure for the positive theory
of *E*_{1}∪*E*_{2}? For theories over
disjoint signatures, this problem was solved by Baader and Schulz in 1995.
This paper is a first step towards extending this result to the case
of theories sharing constructors. Since there is a close connection between
positive theories and unification problems, this also extends to the
non-disjoint case the work on combining decision procedures for unification
modulo equational theories. |
| |