Theorem Proving Using Rigid E-Unification Equational Matings - Jean H. Gallier; Stan Raatz; Wayne Snyder (LICS, 1987)

A General Complete E-Unification Procedure. - Jean H. Gallier; Wayne Snyder (RTA, 1987)

Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Stan Raatz; Wayne Snyder (CADE, 1988)

Rigid E-Unification is NP-Complete - Jean H. Gallier; Wayne Snyder; Paliath Narendran; David A. Plaisted (LICS, 1988)

Efficient Ground Completion: An O(n log n) Algorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E. - Wayne Snyder (RTA, 1989)

Higher-Order Unification Revisited: Complete Sets of Transformations. - Wayne Snyder; Jean H. Gallier (J. Symb. Comput., 1989)

Complete Sets of Transformations for General E-Unification. - Jean H. Gallier; Wayne Snyder (Theor. Comput. Sci., 1989)

Higher Order E-Unification. - Wayne Snyder (CADE, 1990)

An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality. - Wayne Snyder; Christopher Lynch (CTRS, 1990)

Rigid E-Unification: NP-Completeness and Applications to Equational Matings - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (Inf. Comput., 1990)

Goal Directed Strategies for Paramodulation. - Wayne Snyder; Christopher Lynch (RTA, 1991)

Basic Paramodulation and Superposition. - Leo Bachmair; Harald Ganzinger; Christopher Lynch; Wayne Snyder (CADE, 1992)

Theorem Proving Using Equational Matings and Rigid E-Unification. - Jean H. Gallier; Paliath Narendran; Stan Raatz; Wayne Snyder (J. ACM, 1992)

Proof theory for general unification. - Wayne Snyder (Birkhäuser, 1993)

On the Complexity of Recursive Path Orderings. - Wayne Snyder (Inf. Process. Lett., 1993)

An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. - Jean H. Gallier; Paliath Narendran; David A. Plaisted; Stan Raatz; Wayne Snyder (J. ACM, 1993)

A Fast Algorithm for Generating Reduced Ground Rewriting Systems from a Set of Ground Equations. - Wayne Snyder (J. Symb. Comput., 1993)

Automated Deduction with Constraints. - Wayne Snyder (CCL, 1994)

A Tool for Testing Confluence of Production Rules. - James G. Schmolze; Wayne Snyder (EUROVAV, 1995)

Redundancy Criteria for Constrained Completion. - Christopher Lynch; Wayne Snyder (Theor. Comput. Sci., 1995)

Basic Paramodulation - Leo Bachmair; Harald Ganzinger; Christopher Lynch; Wayne Snyder (Inf. Comput., 1995)

Rewrite Semantics for Production Rule Systems: Theory and Applications. - Wayne Snyder; James G. Schmolze (CADE, 1996)

Detecting Redundant Production Rules. - James G. Schmolze; Wayne Snyder (AAAI/IAAI, 1997)

A Fast Algorithm for Uniform Semi-Unification. - Alberto Oliart; Wayne Snyder (CADE, 1998)

Detecting redundancy among production rules using term rewrite semantics. - James G. Schmolze; Wayne Snyder (Knowl. Based Syst., 1999)

Unification Theory. - Franz Baader; Wayne Snyder (Handbook of Automated Reasoning, 2001)

Fast algorithms for uniform semi-unification. - Alberto Oliart; Wayne Snyder (J. Symb. Comput., 2004)