Publication List for Wayne Snyder

Most Recent Publications

• Oliart, A., and W. Snyder, "Fast Algorithms for Uniform Semi-Unification," Journal of Symbolic Computation 37 (2004) 455-484. [ PS | PDF ]
• Baader, F., and W. Snyder, "Unification Theory," chapter eight of Handbook of Automated Deduction, Springer Verlag, Berlin (2001). [ PS | PDF ]

The remainder of this page is a complete list of my publications. Within each section, publications appear in reverse chronological order.

Refereed Journal Articles

• Oliart, A., and W. Snyder, "Fast Algorithms for Uniform Semi-Unification," Journal of Symbolic Computation 37 (2004) 455-484. [ PS | PDF ]
• Lynch, C., and W. Snyder, ``Redundancy Criteria for Constrained Completion,'' Theoretical Computer Science, 142 (1995) 141--177. [ PS | PDF ]
• Bachmair, L., H. Ganzinger, C. Lynch, and W. Snyder, ``Basic Paramodulation,'' Information and Computation 121:2 (1995) 172--192. [ PS | PDF ]
• Snyder, W., ``A Fast Algorithm for Generating Reduced Ground Rewriting Systems from a Set of Ground Equations,'' Journal of Symbolic Computation 15 : 4 (1993) 415-450.
• Gallier, J., P. Narendran, D. Plaisted, S. Raatz, and W. Snyder, ``An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time," Journal of Association for Computing Machinery 40 : 1 (1993) 1--16. [ PDF ]
• Snyder, W., ``On the Complexity of Simplification Orderings,'' Information Processing Letters 46 (1993) 257--262.
• Gallier, J., P. Narendran, S. Raatz, and W. Snyder, ``Theorem Proving Using Equational Matings and Rigid E-Unification," Journal of Association for Computing Machinery 39 : 2 (1992) 377--429. [ PDF ]
• Gallier, J., P. Narendran, D. Plaisted, and W. Snyder, ``Rigid E-Unification: NP-Completeness and Applications to Equational Matings," Information and Computation 87 (1990) 129--195 (special issue of selected papers from LICS 1988).
• Snyder, W., and J. Gallier, ``Higher-Order Unification Revisited: Complete Sets of Transformations,'' Journal of Symbolic Computation 8 (1989) 101--140; reprinted in the book Unification, C. Kirchner (Ed.), Academic Press, San Diego (1990) 565--604.
• Gallier, J., and W. Snyder, ``Complete Sets of Transformations for General E-Unification," Theoretical Computer Science 67 (1989) 203--260.

Conference Papers

• Oliart, A., and W. Snyder, "A Fast Algorithm for Uniform Semi-Unification," Proceedings of 15th CADE, C. Kirchner, Ed., Springer LNCS, Vol. 1452 (1998) 239-253
• Schmolze, J., and W. Snyder, "Detecting Redundant Production Rules," AAAI-97 (1997).
  
• Snyder, W., and J. Schmolze, "Rewrite Semantics for Production Rule Systems: Theory and Applications," CADE-13, LNAI 607 (1996) 508--522.
• Lynch, C., and W. Snyder, ``Redundancy Criteria for Constrained Completion,'' Proceedings of Fifth International Conference on Rewrite Techniques and Applications, C. Kirchner (Ed.), Lecture Notes in Computer Science, Volume 690, Springer-Verlag, Berlin (1993) 2--16.
• Bachmair, L., H. Ganzinger, C. Lynch, and W. Snyder, ``Basic Paramodulation and Superposition,'' Proceedings of 11th Cade, Deepak Kapur (Ed.), Lecture Notes in Artificial Intelligence, Volume 607, Springer-Verlag, Berlin (1992) 462--476.
• Snyder, W., and C. Lynch, ``An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality,'' Proceedings of Second International Workshop on Conditional and Typed Rewriting Systems, S. Kaplan and M. Okada (Eds.), Lecture Notes in Computer Science, Volume 516, Springer-Verlag, Berlin (1991) 454--461.
• Snyder, W., and C. Lynch, ``Goal-Directed Strategies for Paramodulation,'' Proceedings of Fourth International Conference on Rewriting Techniques and Applications, Ronald Book (Ed.), Lecture Notes in Computer Science, Volume 488, Springer-Verlag, Berlin (1991) 150--161.
• Snyder, W., ``Higher-Order E-Unification,'' Proceedings of Tenth International Conference on Automated Deduction, J. Siekmann (Ed.), Lecture Notes in Artificial Intelligence, Volume 449, Springer Verlag, Berlin (1990) 573--587.
• Snyder, W., ``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,'' Proceedings of the Third International Conference on Rewriting Techniques and Applications, Nachum Dershowitz (Ed.), Lecture Notes in Computer Science, Volume 355, Springer-Verlag, Berlin (1989) 419--433.
• Gallier, J., P. Narendran, D. Plaisted, and W. Snyder, ``Rigid E-Unification is NP-Complete," Proceedings of Symposium on Logic in Computer Science, Edinburgh, Scotland (1988) 218--227.
• Gallier, J., P. Narendran, D. Plaisted, S. Raatz, and W. Snyder, ``Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time," Proceedings of 9th CADE, E. Lusk and R. Overbeek, Eds., LNCS, Vol. 310, Springer-Verlag, Berlin (1988) 182--196.
• Gallier, J., S. Raatz, and W. Snyder, ``Theorem Proving Using Rigid E-Unification: Equational Matings," Proceedings of LICS, Ithaca, NY (1987) 338--346.
• Gallier, J., and W. Snyder, ``A General Complete E-Unification Procedure," Proceedings of the Second International Conference on Rewriting Techniques and Applications, Pierre Lescanne (Ed.), LNCS, Vol. 256, Springer-Verlag, Berlin (1987) 216--227.

Books:

• Snyder, W., The Theory of General Unification, in series Progress in Computer Science and Applied Logic, Birkhauser Boston Inc., Boston MA (1991). Amazon.com sales rank in 12/02 was 1,801,206....

Book Chapters:

• Baader, F., and W. Snyder, "Unification Theory," chapter eight of Handbook of Automated Deduction, Springer Verlag, Berlin (2001). [ PS | PDF ]
  
• Schmolze, J., and W. Snyder, ``Using Confluence to Control Parallel Production Systems,'' to appear in the book Parallel Processing for Artificial Intelligence II, H. Kitano, V. Kumar, and C.B. Suttner (Eds.), Elsevier Science Publishers B.V., Amsterdam (1994) (also to appear in Proceedings of the Second International Workshop on Parallel Processing in AI, Chambery, France, August 1993).
• Gallier, J., W.~Snyder, and S.~Raatz, ``Rigid E-Unification and its Application to Matings," in the book Resolution of Equations in Algebraic Structures, Nivat and Ait-Kaci (Eds.), Academic Press, Boston (1988) 151--216.

Other Publications

• Schmolze, J., and W. Snyder, "On the Decidability of Redundancy Testing in Expert Systems," Workshop on Knowledge-Based Systems, AAAI-97 (1997).
• Schmolze, J., and W. Snyder, ``Confluence and Verification for Production Rule Systems,'' to appear in Proceedings of Workshop on Verification and Validation of Expert Systems, held in conjunction with Twelfth National Conference on Artificial Intelligence (AAAI-94).
• Proceedings of the Seventh International Workshop on Unification, F. Baader and W. Snyder (Eds.), Boston University, Boston MA (1994). (See also BUCS Technical Report 1994).
• Proceedings of the Sixth International Workshop on Unification, F. Baader, J. Siekmann, and W. Snyder (Eds.), Dagstuhl Seminar Report 9231, Dagstuhl, Germany (1993). (See also BUCS Technical Report No. 93-001).
• Gallier, J., and W. Snyder, ``Designing Unification Procedures using Transformations: A Survey,'' in Logic from Computer Science, Proceedings of a Workshop held 13-17 November 1989, Y. Moschovakis (Ed.), Mathematical Sciences Research Institute Publications, Volume 21, Springer-Verlag, New York (1992) 153--215. Also appeared in Bulletin of the EATCS 40 (1990) 273--326.