15th International Workshop on Unification (UNIF 2001) to be held in Europe

本项目的主要目标是组织2001年统一理论框架，即第15届统一问题国际讲习班。统一问题涉及到以句法方式或以给定逻辑理论为模来确定给定术语的问题。语法统一是大多数自动推理系统的基本操作，统一模理论可以用来，例如，建立在特殊的方程理论到定理证明。UNIF 2001将是一系列关于统一的年度国际讲习班中的最新一期，以前的讲习班主要在欧洲举行（法国、德国、意大利和西班牙）和两次在美国举行。2001年的UNIF的目的，与以前的会议一样，是把对统一感兴趣的人聚集在一起，（甚至是未完成的）工作，并讨论统一和相关领域的新思想和趋势。特别是，它的目的是为年轻的研究人员和在相关领域工作的研究人员提供一个很好的机会，除了来自自动推理和术语重写的研究人员，UNIF的传统参与者之外，今年的研讨会还将尝试吸引来自理论计算机科学的研究人员，研究特殊理论的统一算法（如关联性），在过去两年中取得了惊人的进展。工作坊还将通过旅行奖励和注册费减免，来自美国的年轻研究人员。这样做的目的是为了刺激研究在这个国家的统一，以及提醒美国研究人员在自动推理和验证在这一领域的最新成果。

The main objective of this project is to organize UNIF 2001,the 15th International Workshop 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. UNIF 2001 will be the latest in a series of annual internationalworkshops on unification, the previous ones having been mostly in Europe (France, Germany, Italy, and Spain) and twice in the US.The aim of UNIF 2001, as that of the previous meetings, 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 theoryand get in contact with the experts in the field.In addition to researchers from automated reasoning and term rewriting, the traditional participants to UNIF, this year's workshop will try to attract also researchers from theoretical computer science working on unification algorithms for special theories (such as associativity) where astonishing progress has been achieved in the last two years.The workshop will also try to facilitate, with travel awards and registration fee waivers, the participation of young researchers from the United States. The intent of this is to stimulate researchon unification in this country, as well as alert US researchers working in automated reasoning and verification to recent results in this field.