| 2009 | CADE | Building Theorem Provers. | Mark E. Stickel |
| 2001 | IJCAI | Balance and Filtering in Structured Satisfiable Problems. | Henry A. Kautz, Yongshao Ruan, Dimitris Achlioptas, Carla P. Gomes, Bart Selman, Mark E. Stickel |
| 2000 | AAAI | Using Prior Knowledge: Problems and Solutions. | Vinay K. Chaudhri, Mark E. Stickel, Jrme Thomr, Richard J. Waldinger |
| 1997 | CADE | A Practical Integration of First-Order Reasoning and Decision Procedures. | Nikolaj S. Bjrner, Mark E. Stickel, Toms E. Uribe |
| 1994 | CADE | Deductive Composition of Astronomical Software from Subroutine Libraries. | Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood |
| 1994 | SP | Elimination of inference channels by optimal upgrading. | Mark E. Stickel |
| 1993 | SP | Detection and elimination of inference channels in multilevel relational database systems. | Xiaolei Qian, Mark E. Stickel, Peter D. Karp, Teresa F. Lunt, Thomas D. Garvey |
| 1992 | CADE | Caching and Lemmaizing in Model Elimination Theorem Provers. | Owen L. Astrachan, Mark E. Stickel |
| 1992 | DBSEC | Toward a Tool to Detect and Eliminate Inference Problems in the Design of Multilevel Databases. | Thomas D. Garvey, Teresa F. Lunt, Xiaolei Qian, Mark E. Stickel |
| 1990 | CADE | A Prolog Technology Theorem Prover. | Mark E. Stickel |
| 1989 | NAACL | TACITUS: A Message Understanding System. | Jerry R. Hobbs, Douglas E. Appelt, John Bear, Mark E. Stickel, Mabry Tyson |
| 1988 | ACL | Interpretation as Abduction. | Jerry R. Hobbs, Mark E. Stickel, Paul A. Martin, Douglas Edwards |
| 1988 | CADE | The KLAUS Automated Deduction System. | Mark E. Stickel |
| 1988 | CADE | A Prolog Technology Theorem Prover. | Mark E. Stickel |
| 1986 | CADE | A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. | Mark E. Stickel |
| 1986 | CADE | The KLAUS Automated Deduction System. | Mark E. Stickel |
| 1985 | IJCAI | Automated Deduction by Theory Resolution. | Mark E. Stickel |
| 1985 | IJCAI | An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction. | Mark E. Stickel, Mabry Tyson |
| 1984 | CADE | A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. | Mark E. Stickel |
| 1983 | AAAI | Theory Resolution: Building in Nonequational Theories. | Mark E. Stickel |
| 1982 | AAAI | A Nonclausal Connection-Graph Resolution Theorem-Proving Program. | Mark E. Stickel |
| 1975 | IJCAI | A Complete Unification Algorithm for Associative-Commutative Functions. | Mark E. Stickel |
| 1973 | IJCAI | A Hole in Goal Trees: Some Guidance from Resolution Theory. | Donald W. Loveland, Mark E. Stickel |