RTA on Wednesday

Detailed program
Wednesday July 24th, 2002
See also the unified by-slot program

All sessions take place in auditorium 3.

Session 9

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.

Session 10

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.

Session 11

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 E1 and E2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of E1E2? 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.