Rewriting techniques and applications, RTA'91
Hélène Kirchner, Pierre Lescanne · ACM SIGACT News · 1991
The fourth Conference of Rewriting Techniques and Applications took place in the beautiful Centro di Cultura Scientifica "A .Volta" at Villa Olmo, a nice mansion on the shore o f Como Lake .In addition to this wonderful accommodation and perfect organization due t o the department of computer science of the University of Milano, the conference was of very high quality and Ronald Book deserves credit for his very good job .In what follows we tr y to identify current trends in the field of rewriting and classify the contributions according t o them .Of course, several papers deal with different topics and this classification is subjective .The proceedings of the conference are published by Springer Verlag as the Lecture Notes i n Computer Science volume 488 .Note that RTA'93 will take place somewhere in the USA .1 Unification, narrowing, paramodulatio n Unification and especially equational (or semantic) unification stay at the kernel of the fiel d and is present at RTA'91 with not less than ten papers .• Syntactic theories are interesting because unification procedures can be automatically provided for them .Undecidable properties of syntactic theories are proved by F. Klay: unifiability in syntactic theories is not decidable and syntacticness of a theory is eve n not semi-decidable .Therefore it becomes apparent that some additional property ha s to be added to syntacticness in order to get decidability results .• In AC-Unification through Order-Sorted AC1-Unification, a new algorithm is presented by E .Domenjoud for unification modulo Associativity and Commutativity .It is achieved by adding axioms expressing the existence of an identity for every ACoperator and working in the AC1-theory .In order to get a conservative extension o f the quotient algebra, an order-sorted framework is introduced .• Unification, Weak unification, Upper Bound, Lower Bound, and Generalization Problems in an equational theory are studied by F .Baader .Instantiation preorders on solutions influence the existence of solutions for these problems, according to the se t of variables where substitutions are compared.• In Adding homomorphisms to commutative/monoidal theories, F .Baader and W. Nut t consider the class of theories, called commutative or monoidal, where unification i s