 | |
Sessions
take place in auditorium 3 unless otherwise indicated.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. |
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
P→N←Q completing a span P←M→Q, 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". |
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. |
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. |
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. |
Chair:
Aart Middeldorp Joint
with FME, LICS
Room:
City Hall | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
