Introduction to the special issue: Unification

In the days of its foundation, the field of science covered by UNIF – a series of annual international workshops on unification – was still in its infancy. With the advent of automated reasoning, term rewriting, logic programming, natural language processing, and program analysis, the areas of computer science concerned by unification were seething with excitement. With the coming out of researches in constraint solving and admissibility of inference rules and with the breaking out of applications, such as type checking, query answering, and cryptographic protocol analysis, the development of unification was not long in going at full speed.

Compositional Specification in Rewriting Logic

Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. We discuss the motivations and implications of our proposal, formalize it for rewriting logic and also for transition structures, to be used as semantics, and show the power of our approach with some examples.