UNIF on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program

All sessions take place in auditorium 8.

Session 4

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.

Session 5

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

Session 6

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 ACUIHC (`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.

Session 7

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