Mark E. Stickel

Principal Scientist
Artificial Intelligence Center

Mark E. Stickel                 Internet: stickelai.sri.com
Artificial Intelligence Center
SRI International
333 Ravenswood Avenue
Menlo Park, California 94025

Research Areas

• Automated Deduction
• Natural Language Processing
• Computer Security

Honors

• 2002 Herbrand Award for Distinguished Contributions to Automated Reasoning
• Elected Fellow of American Association for Artificial Intelligence, 1992

Software Systems

• PTTP - Prolog Technology Theorem Prover
• LDPP' - List-Based Davis-Putnam Prover
• SNARK - SRI's New Automated Reasoning Kit
• Amphion - Knowledge-Based Software Engineering
• DISSECT - Database Inference System Security Tool
• FASTUS - Finite State Automaton Text Understanding System
• QPQ - Repository for Deductive Software

Selected Publications

• Formatted publications
• Bibtex publications
• A Unification Algorithm for Associative-Commutative Functions

  Mark E. Stickel
  Journal of the ACM (JACM), 1981
• Complete Sets of Reductions for Some Equational Theories

  Gerald E. Peterson, Mark E. Stickel
  Journal of the ACM (JACM), 1981
• Stickel, M.E. Automated deduction by theory resolution. Journal of Automated Reasoning 1, 4 (1985), 333-355.
• Stickel, M.E. A Prolog technology theorem prover: implementation by an extended Prolog compiler. Journal of Automated Reasoning 4, 4 (December 1988), 353-380.
• Stickel, M.E. A Prolog technology theorem prover: a new exposition and implementation in Prolog. Theoretical Computer Science 104 (1992), 109-128.
• Stickel, M.E. A Prolog technology theorem prover: a new exposition and implementation in Prolog. Technical Note 464, Artificial Intelligence Center, SRI International, Menlo Park, California, June 1989. (longer version of above reference that includes annotated code)
• Stickel, M.E. The path-indexing method for indexing terms. Technical Note 473, Artificial Intelligence Center, SRI International, Menlo Park, California, October 1989.
• Stickel, M.E. A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation. Annals of Mathematics and Artificial Intelligence 4 (1991), 89-106.
• Hobbs, J.R., M.E. Stickel, D.E. Appelt, and P. Martin. Interpretation as abduction. Artificial Intelligence 63, 1-2 (1993), 69-142.
• Zhang, H. and M.E. Stickel. Implementing the Davis-Putnam method. Journal of Automated Reasoning 24, 1-2 (February 2000), 277-296.
• Slaney, J., M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: quasigroup existence problems. Computers and Mathematics with Applications 29 (1995), 115-132.
• Uribe, T.E. and M.E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Germany, September 1994, 34-49.
• Stickel, M., R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astronomical software from subroutine libraries. Proceedings of the Twelfth International Conference on Automated Deduction (CADE-12), Nancy, France, June 1994, 341-355.

Downloads

• Common Lisp multiple-value-binding let form
• Quasigroup example generator
• Downloads are also listed in pages for software systems

AI Center Home Page

SRI International Home Page

Mark E. Stickel (stickelai.sri.com)