| Unification theory F Baader, W Snyder Handbook of automated reasoning 1, 445-532, 2001 | 1026 | 2001 |
| Higher-order unification revisited: Complete sets of transformations W Snyder, J Gallier Journal of Symbolic Computation 8 (1-2), 101-140, 1989 | 223 | 1989 |
| Basic paramodulation L Bachmair, H Ganzinger, C Lynch, W Snyder Information and computation 121 (2), 172-192, 1995 | 214 | 1995 |
| Complete sets of transformations for general E-unification JH Gallier, W Snyder Theoretical Computer Science 67 (2-3), 203-260, 1989 | 177 | 1989 |
| Basic paramodulation and superposition L Bachmair, H Ganzinger, C Lynch, W Snyder International Conference on Automated Deduction, 462-476, 1992 | 158 | 1992 |
| A proof theory for general unification W Snyder Springer Science & Business Media, 2012 | 113 | 2012 |
| Rigid E-unification: NP-completeness and applications to equational matings J Gallier, P Narendran, D Plaisted, W Snyder Information and Computation 87 (1-2), 129-195, 1990 | 92 | 1990 |
| Theorem proving using rigid E-unification: Equational matings JH Gallier, S Raatz, W Snyder University of Pennsylvania, School of Engineering and Applied Science …, 1987 | 92 | 1987 |
| Theorem proving using equational matings and rigid E-unification J Gallier, P Narendran, S Raatz, W Snyder Journal of the ACM (JACM) 39 (2), 377-430, 1992 | 83 | 1992 |
| A general complete E-unification procedure JH Gallier, W Snyder International Conference on Rewriting Techniques and Applications, 216-227, 1987 | 75 | 1987 |
| A fast algorithm for generating reduced ground rewriting systems from a set of ground equations W Snyder Journal of Symbolic Computation 15 (4), 415-450, 1993 | 64 | 1993 |
| Higher order E-unification W Snyder International Conference on Automated Deduction, 573-587, 1990 | 47 | 1990 |
| An algorithm for finding canonical sets of ground rewrite rules in polynomial time J Gallier, P Narendran, D Plaisted, S Raatz, W Snyder Journal of the ACM (JACM) 40 (1), 1-16, 1993 | 44 | 1993 |
| Goal directed strategies for paramodulation W Snyder, C Lynch International Conference on Rewriting Techniques and Applications, 150-161, 1991 | 40 | 1991 |
| Unification theory. Handbook of Automated Reasoning F Baader, W Snyder Alan Robinson, Andrei Voronkov, eds 1, 446-533, 2001 | 39 | 2001 |
| Handbook of Automated Reasoning, chapter Unification Theory F Baader, W Snyder Elsevier, 2001 | 34 | 2001 |
| 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 W Snyder Rewriting Techniques and Applications: 3rd International Conference, RTA-89 …, 1989 | 33 | 1989 |
| Designing unification procedures using transformations: A survey JH Gallier, W Snyder Logic from Computer Science: Proceedings of a Workshop held November 13–17 …, 1992 | 32 | 1992 |
| Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time J Gallier, P Narendran, D Plaisted, S Raatz, W Snyder 9th International Conference on Automated Deduction: Argonne, Illinois, USA …, 1988 | 30 | 1988 |
| Redundancy criteria for constrained completion C Lynch, W Snyder Theoretical computer science 142 (2), 141-177, 1995 | 28 | 1995 |