RTA on Monday

Detailed program
Monday July 22nd, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

FLoC opening

Joint with FME, LICS
Room: auditorium 1
Chair: Moshe Vardi

08:45-08:55  Introduction and welcome

08:55-09:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof
The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these "little engines of proof" and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modern reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.

Session 1

Chair: Daniel J. Dougherty

10:00-10:30  Paul-André Melliès, U Paris VII, France
Axiomatic rewriting theory VI: Residual theory revisited
Residual theory is the algebraic theory of confluence for the λ-calculus, and more generally conflict-free rewriting systems (without critical pairs). The theory took its modern shape in Lévy's PhD thesis, after Church, Rosser and Curry's seminal steps. There, Lévy introduces a permutation equivalence between rewriting paths, and establishes that among all confluence diagrams PNQ completing a span PMQ, there exists a minimum such one, modulo permutation equivalence. Categorically, the diagram is called a pushout.
In this article, we extend Lévy's residual theory, in order to enscope "border-line" rewriting systems, which admit critical pairs but enjoy a strong Church-Rosser property (existence of pushouts.) Typical examples are the associativity rule and the positive braid rewriting systems. Finally, we show that the resulting theory reformulates and clarifies Lévy's optimality theory for the λ-calculus, and its so-called "extraction procedure".

Session 2

Chair: Thérèse Hardin

11:00-11:30  Richard Kennaway, U East Anglia, UK
Zurab Khasidashvili, Bar-Ilan U, Israel
Adolfo Piperno, U Rome I (La Sapienza), Italy
Static analysis of modularity of beta-reduction in the hyperbalanced lambda-calculus
We investigate the degree of parallelism (or modularity) in the hyperbalanced λ-calculus, λH, a subcalculus of λ-calculus containing all simply typable terms (up to a restricted η-expansion). In technical terms, we study the family relation on redexes in λH, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced λ-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of β-reduction.

11:30-12:00  Germain Faure, ENS Lyon, France
Claude Kirchner, LORIA Nancy, France
Exceptions in the rewriting calculus
In the context of the rewriting calculus, we introduce and study an exception mechanism that allows us to express in a simple way rewriting strategies and that is therefore also useful for expressing theorem proving tactics. The proposed exception mechanism is expressed in a confluent calculus which gives the ability to simply express the semantics of the FIRST tactical and to describe in full details the expression of conditional rewriting.

12:00-12:30  Georg Struth, U Augsburg, Germany
Deriving focused lattice calculi
We derive rewrite-based ordered resolution calculi for semilattices, distributive lattices and boolean lattices. Using ordered resolution as a metaprocedure, theory axioms are first transformed into independent bases. Focused inference rules are then extracted from inference patterns in refutations. The derivation is guided by mathematical and procedural background knowledge, in particular by ordered chaining calculi for quasiorderings (forgetting the lattice structure), by ordered resolution (forgetting the clause structure) and by Knuth-Bendix completion for non-symmetric transitive relations (forgetting both structures). Conversely, all three calculi are derived and proven complete in a transparent and generic way as special cases of the lattice calculi.

Session 3

Chair: Ralf Treinen

14:00-14:30  Hiroyuki Seki, Nara Inst. of Science and Techn., Japan
Toshinori Takai, AIST, Japan
Youhei Fujinaka, Nara Inst. of Science and Techn., Japan
Yuichi Kaji, Nara Inst. of Science and Techn., Japan
Layered transducing term rewriting system and its recognizability preserving property
A term rewriting system which effectively preserves recognizability (EPR-TRS) has good mathematical properties. In this paper, a new subclass of TRSs, layered transducing TRSs (LT-TRSs) is defined and its recognizability preserving property is discussed. The class of LT-TRSs contains some EPR-TRSs, e.g., {f(x)→f(g(x))} which do not belong to any of the known decidable subclasses of EPR-TRSs. Bottom-up linear tree transducer, which is a well-known computation model in the tree language theory, is a special case of LT-TRS. We present a sufficient condition for an LT-TRS to be an EPR-TRS. Also some properties of LT-TRSs including reachability are shown to be decidable.

14:30-15:00  Hitoshi Ohsaki, AIST, Japan
Toshinori Takai, AIST, Japan
Decidability and closure properties for computation on equational tree languages
Equational tree automata provide a powerful tree language framework that facilitates to recognize congruence closures of tree languages. In the paper we show the emptiness problem for AC-tree automata and the intersection-emptiness problem for regular AC-tree automata, each of which was open in our previous work, are decidable, by a straightforward reduction to the reachability problem for ground AC-term rewriting. The newly obtained results generalize decidability of so-called reachable property problem of Mayr and Rusinowitch. We then discuss complexity issue of AC-tree automata. Moreover, in order to solve some other questions about regular A- and AC-tree automata, we recall the basic connection between word languages and tree languages.

15:00-15:30  Pierre Réty, U Orléans, France
Julie Vuotto, U Orléans, France
Regular sets of descendants by some rewrite strategies
For a constructor-based rewrite system R, a regular set of ground terms E, and assuming some additional restrictions, we build a finite tree automaton that recognizes the descendants of E, i.e. the terms issued from E by rewriting, according to innermost, innermost-leftmost, and outermost strategies.

Session 4

Chair: Aart Middeldorp

16:00-16:30  Johannes Waldmann, U Leipzig, Germany
Rewrite games
In this note, we propose some challenging problems related to certain rewrite games. In particular, we re-formulate an open problem from combinatorial game theory (do all finite octal games have an ultimately periodic Sprague-Grundy sequence?) as a question about rationality of some tree languages.
We propose to attack this question by methods from set constraint systems, and show some cases where this works directly.
Finally we present rewrite games from to combinatory logic, and their relation to algebraic tree languages.

16:30-17:30  Business meeting

Chair: Aart Middeldorp

19:00-21:00  City Hall reception

Joint with FME, LICS
Room: City Hall