UNIF '89 : Extended Abstracts of the Third International Workshop on Unification, 1989, [Lambrecht, FR Germany, Monday, June 26th - Wednesday, 28th 1989]

Abstract

This is a collection of extended abstracts of the talks given at the Third International Workshop on Unification (UNIF’89) hold during June 26th - 28th, 1989 in the PFALZAKADEMIE at Lambrecht, Germany. The workshop is a forum for the researchers that are interested in Unification Theory and its applications, and we met since 1986 every year to exchange and discuss results, ideas and new trends in this area. Topics of the unification workshops are • Narrowing • Typed Unification • General E-Unification & Calculi • Foundations • Implementations • Applications • Special Unification Algorithms • Combination Problems • Disunification • Constraint Solving This 3rd Workshop on Unification had 49 participants from Belgium, France, Germany, Great Britain, and the USA. We had 10 short and 18 long talks, several system demonstrations, and an excursion to the Weingut Schonhof with a wine tasting presented by Philip Scammel and a banquet speech about living with limited vocabulary by Pierre Lescanne. The volume is organized as follows. There are seven sections, each with three to five abstracts, essentially in the order of presentation at Lambrecht. The first section is about General E-Unification & Combination and contains papers on Higher Order E-Unification (J. Gallier, W. Snyder, V. Tannen) and its connection to first-order rewriting and on the translation of proofs from one proof system into another one (Proof Transformations For Simple Equational Theories, T.Nipkow). These are followed by presentations about combination methods for regular and collapse-free theories applied to AC-unification (A New Combination Technique for AC-Unification, A. Boudet) and combination methods for general theories (Optimizations of Schmidt-Schauß’ General Unification Procedure, M. Tepp). The second section is on Applications of unification in the field of Completion of term rewriting systems. It begins with a paper by P. Watson and A.J.J. Dick on Least Sorts in Order-Sorted Rewriting. They attack the problem of non-uniquely determined sorts of terms during rewriting by introducing dynamic sorts. The second paper is by U. Martin and T. Nipkow on Order-sorted Rewriting and Confluence. Some ideas in constructing completion procedures are given by P. Lescanne in his paper Completion Procedures as Transition Rules + Control at the end of this section. Third section is on Foundations starting with W. Nutt’s Unification in Modular Categories. This is followed by Unification in Commutative Theories, Hilbert's Basis Theorem, and Grobner Bases (F. Baader). The next paper is by F. Klay and C. Kirchner, A Note on Syntactic Theories. The section closes with two papers on decidability: On the Decidability ofthe Unification Problem by A. Bockmayr and W.Nutt with The Unification Hierarchy is Undecidable. The next section on Typed Unification begins with a paper by G. Smolka: Polymorphically Order Sorted Unification. L. Duponcheel presents a paper on Typed Algebra, followed by U. Waldmann with Unitary Unification in Order-sorted Signatures. Finally E. Domenjoud shows a way to do AC-Unification Through Order SortedAC1-Unification. The two sections on Special Algorithms start with a the contribution of H. Abdulrab and J.-P. Pecuchet on Associative Unification followed by two presentations on solving systems of diophantine equations. The first of them contains a generalization of Fortenbacher's algorithm to solve linear diophantine equations to a procedure that solves systems of linear diophantine equations in an efficient way (E. Contejean, H. Devie: Solving Systems of Linear Diophantine Equations). The second one gives some boundaries on the size of Solutions of a Linear Diophantine System (J.-F. Romeuf). Finally H.J. Ohlbach presents an advantageous representation of terms, Abstraction Tree Indexing for Terms. The second section on Special Algorithms is started with S. Holldobler's paper Unification over Rational Trees, that is unification of terms that may be cyclic. He is followed by L. Pottier and his presentation on Term Generalizations in the AC Case. H. Leiß comes up with a procedure for a process that might be seen as a common generalization of unification and matching: A Semi-Unification Algorithm. Finally B. Gramlich presents some ideas on the Unification of Term Schemes. The last section, Equational Problems & Constraint Solving, begins with C. and H. Kirchner’s Constrained Equational Reasoning. The topic of Order Sorted Algebras is again taken up by H. Comon in his paper on Equational Problems in Order Sorted Algebras. H. Aït-Kaci presents his quite technical work on structured types (Disjunctive Ψ-Term Unification). The last paper of the workshop is by L. Puel and A. Suarez, Unification of Restricted Terms. The volume is closed with an appendix containing the list of wines we tasted at Weingut Schonhof, an abstract of the banquet speech by P. Lescanne on the Life with a Limited Vocabulary, and of course the list of participants. We would like to thank the authors, without whom the workshop would never have taken place. We also thank the staff of the PFALZAKADEMIE who provided an inspiring atmosphere and supported the organization of the workshop. Thanks also to Dorothea Kilgore and Patricia Sarach who had the not always easy job of assisting with organization and registration. Gebhardt Pzyrembel prepared the system demonstrations and SUN Germany provided machines for these demos. Finally we thank Volkswagen-Stiftung for their financial support of the workshop. We hope to meet most people again at the next Workshop on Unification that will take place in Leeds, Great Britain, in July 1990 and will be organized by John K. Truss. August, 1989 Hans-Jürgen Bürckert and Werner Nutt