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

点击翻译按钮获取中文摘要

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.