Termination of Nested and Mutually Recursive Algorithms
Deduction Trees and the View Update Problem in Indefinite Deductive Databases
Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories*
The Use of Lemmas in the Model Elimination Procedure