Matching with Distributivity. - Jalel Mzali (CADE, 1986)

SbReve2: A Term Rewriting Laboratory with (AC-) Unfailing Completion. - Siva Anantharaman; Jieh Hsiang; Jalel Mzali (RTA, 1989)