TeReSe

The next TeReSe, an afternoon with presentations on rewriting, will take place on Thursday December 14th 2006 at

De Uithof
in Utrecht

TeReSes take place at locations with an active rewriting community, in or close to the Netherlands (Aachen, Amsterdam, Eindhoven, Utrecht).

Hope to see you.
Vincent van Oostrom

Schedule

13.30 Ariya Isihara (VU Amsterdam): Tree Ordinals and Hydra Games
14.15 Rene Thiemann (RWTH Aachen): SAT Solving for Argument Filterings
15:00 break
15.30 Hans Zantema (TU/e): SAT Solving for Semantic Labelling
16.15 Vincent van Oostrom (UU): Modularity of Constructive Confluence
17.00 end

Afterwards there will be the opportunity to eat out together.

Abstracts

Tree Ordinals and Hydra Games:
Tree ordinals are one of the simplest way to represent countable ordinals. Hydra games originate from Kirby and Paris (1982) as a result in the area of proof theory. In this talk we study a close relation between them; the reduction graph of a hydra coincides to a tree ordinal, and thus the productivity of a system on tree ordinals can be witnessed by the termination of hydra games.

SAT Solving for Argument Filterings:
We introduce a propositional encoding for lexicographic path orders (LPO) in connection with dependency pairs. This facilitates the application of SAT solvers for termination analysis of term rewrite systems based on the dependency pair method. We address two main inter-related issues and encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (1) the combined search for an LPO together with an argument filtering to orient a set of inequalities; and (2) how the choice of the argument filtering influences the set of inequalities that have to be oriented.

We also developed a related encoding for polynomial orders (where the corresponding argument filtering is implicit). Our SAT encodings for both the LPO and polynomial orders were implemented in the termination prover AProVE. Extensive experiments show that by our encodings and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.

SAT Solving for Semantic Labelling:
Until now in termination tools semantic labelling was applied by trying several labellings and then try other techniques. In case of large search spaces applying SAT instead is more appropriate. In this talk we show how the search for a combination of labelling with either polynomial interpretations or matrix interpretations can be done by generating a formula and one call to a SAT solver.

Modularity of Constructive Confluence:
We prove modularity of constructive confluence for term rewriting systems using a novel decomposition of terms into tall aliens and bases. The proof is modular itself in that it factors through the decreasing diagrams theorem for abstract rewriting systems.

After recapitulating modularity of confluence, we introduce the notion of constructive confluence and show that none of the classical proofs yields its modularity. After recapitulating the decreasing diagrams method, we show that it does yield modularity of constructive confluence, generalizing and at the same time simplifying the known results.