UNIF 2001: Call for Participation

                     1st Call for Participation
                              UNIF 2001
               15th International Workshop on Unification
                           June 18-19, 2001
                            Siena,  Italy
                          Part of IJCAR 2001

UNIF is the main international meeting on unification. Unification is
concerned with the problem of identifying given terms, either
syntactically or modulo a given logical theory. Syntactic unification
is the basic operation of most automated reasoning systems, and
unification modulo theories can be used, for instance, to build in
special equational theories into theorem provers.

The main purpose of UNIF is to bring together people interested in
unification, present recent (even unfinished) work, and discuss new
ideas and trends in unification and related fields. In particular, it
is intended to offer a good opportunity for young researchers and
researchers working in related areas to get an overview of the current
state of the art in unification theory and get in contact with the
experts in the field.

The meeting will include short (15 minute) and long (30 minute) talks,
invited talks, and social time to discuss current topics of interest,
which include (but are not limited to):

   o  General E-unification and Calculi 
   o  Special Unification Algorithms
   o  Matching 
   o  Narrowing 
   o  Higher-Order Unification 
   o  Combination problems 
   o  Disunification 
   o  Typed Unification 
   o  Constraint Solving 
   o  Unification Calculi 
   o  Applications 
   o  Implementations 
   o  Type Checking and Reconstruction 
   o  Unification-Based approaches to Grammar 
   o  Applications
   o  Implementations 

All UNIF participants must register to IJCAR. Please refer to the 
IJCAR web page for registration instructions and deadlines.
Please note that the deadline for early registrations is May 15.

Franz Baader   (RWTH Aachen, Germany) 
Volker Diekert (Universit"at Stuttgart, Germany) 
Cesare Tinelli (University of Iowa, USA) 
Ralf Treinen   (Universite' Paris-Sud, France) 

Invited Speakers
Claudio Gutierrez  (Universidad de Chile, Santiago, Chile)
Paliath Narendran  (SUNY at Albany, USA)
Andrei Voronkov    (University of Manchester, UK)

Accepted Talks:

Uniform E-Semi-Unification, by A. Oliart and V. Perez

A Superposition Based Methodology to Design Satisfiability Decision
Procedures, by A. Armando, S. Ranise and M.  Rusinowitch 

Combining Decision Procedures for Positive Theories, by C. Tinelli

Solving Matching Problems in Unions of Non-Disjoint Equational
Theories, by C. Ringeissen

Unification in the empty and flat theories with sequence variables and
flexible arity symbols, by Temur Kutsia

Unification and Projectivity in Propositional Logic, by S. Ghilardi 

Solving Linear Equations over Regular Languages, by F. Baader and R. Kuesters 
Solving Knuth-Bendix ordering constraints, by K. Korovin and A. Voronkov 
Context Congruence Closure and Context Rewriting for Commutative
Context-Free Grammars, by S. Anantharaman

Theories of equations in finitely presented groups, by M. Lohrey 
Parametrized Rewriting on Words, by Benjamin Monate 
Second-Order Schema Matching Based on Projection Point Labeling, by
K. Yamada, K. Hirata and M. Harao

Complexity of Unification and Matching Problems in the Varieties of
Idempotent Semigroups, by Ondrej Klim

On the Complexity of Bounded Second Order Unification, by M. Schmidt-Schauss 
Approximating E-Unification, by C. Lynch and B. Morawska 
Non-Structural Subtype Entailment in Automata Theory, by J. Niehren
and T. Priesnitz

For further information, please visit the UNIF 2001 web site at

Ralf Treinen,      L.R.I. Bât. 490,     Université Paris-Sud,
F91405 Orsay cedex, France.        http://www.lri.fr/~treinen