| | All
sessions take place in auditorium 8.09:00- | 10:00
| Nachum Dershowitz, Tel Aviv U,
Israel Claude
Kirchner, LORIA Nancy, France Invited
talk: **Abstract canonical inference systems** We
provide a general proof theoretical setting under which the
so-called "completion processes"
(as used for equational reasoning) can be modeled, understood, studied,
proved and generalized. This framework - based on a
well-founded ordering on proofs - allows us to derive
saturation processes and redundancy criteria abstractly. |
10:00- | 10:30
| Silvio Ranise, LORIA Nancy, France
**A
superposition decision procedure for the logic of equality with
interpreted and uninterpreted functions** The
logic of equality with uninterpreted functions has been
proved useful in many verification efforts, such the verification of
pipelined microprocessors. Uninterpreted functions allow to abstract from
unimportant details and make the proof obligations amenable to "push-button"
verification methods.
However, it is often the case that some functions must be (partially)
interpreted to successfully check some property. In this abstract, we
present a decision procedure for the logic of uninterpreted functions which
is capable of reasoning modulo a background theory which (partially)
interprets a subset of the functions. We combine well-known techniques of
the rewriting approach to automatic theorem proving, such as saturation and
clausal normal form transformation. We also report on preliminary
experimental results. |
11:00- | 11:30
| Leo Bachmair, State U of New York-Stony
Brook, USA Christelle
Scharff, Pace U, USA
**Direct
combination of completion and congruence closure** Theories
presented by finite sets of ground equations are known
to be decidable. There are different approaches to dealing with ground
equational theories. Researchers interested in term rewriting have applied
completion, a method that transforms a given set of equations into a set of
directed rules that is both terminating and confluent. A rather distinct
approach to solving word problems for ground equational theories is based
on the computation of the so-called congruence closure of a relation. In
this work we bridge the gap between the two approaches and provide a better
understanding of the connection between completion and congruence closure
by defining a new, efficient congruence closure method that integrates key
ideas of completion and graph-based methods of congruence closure in a
novel, direct and natural way. |
11:30- | 12:00
| Mircea Marin, U Tsukuba, Japan Aart
Middeldorp, U Tsukuba, Japan
**New
completeness results for lazy conditional narrowing** We
show the completeness of a lazy conditional narrowing calculus
(LCNC) with leftmost selection for the class of confluent deterministic
conditional rewrite systems (CTRSs). Rewrite rules in deterministic CTRSs
may have extra variables in right-hand sides and conditions. From the
completeness proof we obtain several insights to make the calculus more
deterministic. Furthermore, and similar to the refinements developed for
the unconditional case, we succeeded in removing almost all non-determinism
due to the choice of the inference rule of LCNC by imposing further
syntactic conditions on the participating CTRSs and restricting the set of
solutions for which completeness needs to be established. |
12:00- | 12:30
| Konstantin Korovin, U Manchester, UK Andrei
Voronkov, U Manchester, UK
**The
decidability of the first-order theory of the Knuth-Bendix
orders in the case of unary signatures** |
14:00- | 15:00
| Christopher Lynch, Clarkson U, USA Invited
talk: **Decidability and complexity of ***e*-unification for some classes
of equational theories
*E*-unification
is, in general, an
undecidable problem. We discuss some classes of theories that have been
shown to be decidable, and whose complexity has been analyzed. These
classes have either been defined by a syntactic criteria, or by closure
under some inference rule. We consider completion-based inference systems
and goal-directed inference systems, but we concentrate on goal-directed
inference systems. We discuss some methods of showing that an *E*-unification procedure terminates, and show how
those methods are used prove some classes to be decidable and to analyze
their complexity. |
15:00- | 15:30
| Siva Anantharaman, U
Orléans, France Paliath
Narendran, State U of New York-Albany, USA Michaël
Rusinowitch, LORIA Nancy, France
**ACID-unification,
rewrite reachability and set constraints** In
this paper we study the *E*-unification problem w.r.t. theories extending
*ACI* or *ACUI*.
Particular cases of interest are *ACID* and
*ACUID*, where *ACI* (resp. *ACUI*) is enhanced
with the distributivity laws for a given `*' over an
*ACI* (resp. *ACUI*) symbol `+'; these theories are
useful in program specification based on set constraints. We first look at
the unification problem w.r.t. a theory *ACUIH*^{C} (`*ACUI* plus a set of commuting homomorphisms') situated between
*ACUI* and *ACUID*, and show the problem to be undecidable; the
proof is
via reduction from the reachability problem for Minsky machine
configurations. From this we deduce that *AC*(*U*)*ID*
unification is also undecidable, if
equations of associativity-commutativity or just of associativity on `*', are
added on to *AC*(*U*)*ID*. If no further law on `*' is assumed
other than distributivity over`+', then *ACID*-unification reduces to
solving a set constraints problem with *finite, non-empty*
sets. We present an approach based on labeled dag automata to show that it
is NEXPTIME-decidable. A DEXPTIME lower bound is obtained by other
considerations. These conclusions also hold for *ACUID*-unification. |
16:00- | 16:30
| Franz Baader, Dresden U of Techn., Germany Cesare
Tinelli, U Iowa, USA
**ACU-unification
with a successor symbol** Unification
in the presence of an associative-commutative binary
function symbol + with a unit element 0 (ACU-unification) is
well-investigated. This note is concerned
with what happens if the signature is extended by a successor symbol *s*
that satisfies the usual equation w.r.t. +, i.e., *x*+*s*(*y*)=*s*(*x*+*y*). We show
that unification in the theory obtained this way is basically the same as
ACU-unification with an additional free constant symbol. |
16:30- | 17:00
| Quang Huy Nguyen, LORIA Nancy, France
**A
constructive decision procedure for equalities modulo AC** We
provide in this paper an optimised constructive decision
procedure for AC equalities based on the *syntacticness* of
AC theories. The main idea is to reduce the search space by considering
only terms in associative canonical form. This decision procedure has been
used in the context of an ELAN based tactic for rewriting modulo AC in Coq
where the proofs of AC equalities are efficiently searched by ELAN and
checked in Coq. |
17:00- | 17:30
| Iliano Cervesato, ITT Industries, USA
**Solution
count for multiset unification with trailing multiset
variables** We
consider a subproblem of AC1 unification applied to multisets,
where the expressions being unified mention at most one multiset variable.
This extends the unification problem of lists in Prolog-like languages with
commutativity. We give an upper bound to the number of solutions and
outline an algorithm for their generation. |
17:30- | 17:45
| Business
Meeting |
| |