A Complete Unification Algorithm for Associative-Commutative Functions. - Mark E. Stickel (IJCAI, 1975)

A Hole in Goal Trees: Some Guidance from Resolution Theory. - Donald W. Loveland; Mark E. Stickel (IEEE Trans. Computers, 1976)

Fuzzy four-valued logic for inconsistency and uncertainty. - Mark E. Stickel (MVL, 1978)

Complete Sets of Reductions for Some Equational Theories. - Gerald E. Peterson; Mark E. Stickel (J. ACM, 1981)

A Unification Algorithm for Associative-Commutative Functions. - Mark E. Stickel (J. ACM, 1981)

A Nonclausal Connection-Graph Resolution Theorem-Proving Program. - Mark E. Stickel (AAAI, 1982)

Theory Resolution: Building in Nonequational Theories. - Mark E. Stickel (AAAI, 1983)

A note on leftmost innermost term reduction. - Mark E. Stickel (SIGSAM Bull., 1983)

A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. - Mark E. Stickel (CADE, 1984)

A Prolog Technology Theorem Prover. - Mark E. Stickel (New Gener. Comput., 1984)

An Introduction to Automated Deduction. - Mark E. Stickel (Advanced Course: Fundamentals of Artificial Intelligence, 1985)

An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction. - Mark E. Stickel; Mabry Tyson (IJCAI, 1985)

Automated Deduction by Theory Resolution. - Mark E. Stickel (J. Autom. Reason., 1985)

Set Theory in First-Order Logic: Clauses for Gödel's Axioms. - Robert S. Boyer; Ewing L. Lusk; William McCune; Ross A. Overbeek; Mark E. Stickel; Larry Wos (J. Autom. Reason., 1986)

Schubert's Steamroller Problem: Formulation and Solutions. - Mark E. Stickel (J. Autom. Reason., 1986)

A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification. - Mark E. Stickel (J. Autom. Reason., 1987)

Interpretation as Abduction. - Jerry R. Hobbs; Mark E. Stickel; Paul A. Martin; Douglas Edwards (ACL, 1988)

The KLAUS Automated Deduction System. - Mark E. Stickel (CADE, 1988)

Opening the AC-Unification Race. - Hans-Jürgen Bürckert; Alexander Herold; Deepak Kapur; Jörg H. Siekmann; Mark E. Stickel; Michael Tepp; Hantao Zhang 001 (J. Autom. Reason., 1988)

A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. - Mark E. Stickel (J. Autom. Reason., 1988)

Rationale and Methods for Abductice Reasoning in Natural-Language Interpretation. - Mark E. Stickel (Natural Language and Logic, 1989)

More Advanced and Powerful Proof Tools. - Mark E. Stickel (IFIP Congress, 1989)

TACITUS: A Message Understanding System. - Jerry R. Hobbs; Douglas E. Appelt; John Bear; Mark E. Stickel; Mabry Tyson (HLT (2), 1989)

Monotonicity Properties in Automated Deduction. - Zohar Manna; Mark E. Stickel; Richard Waldinger (Artificial and Mathematical Theory of Computation, 1991)

PTTP and Linked Inference. - Mark E. Stickel (Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991)

Abductive and Approximate Reasoning Models for Characterizing Inference Channels. - Thomas D. Garvey; Teresa F. Lunt; Mark E. Stickel (CSFW, 1991)

A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation. - Mark E. Stickel (Ann. Math. Artif. Intell., 1991)

Caching and Lemmaizing in Model Elimination Theorem Provers. - Owen L. Astrachan; Mark E. Stickel (CADE, 1992)

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 (DBSec, 1992)

Proving Properties of Rule-Based Systems. - Richard J. Waldinger; Mark E. Stickel (Int. J. Softw. Eng. Knowl. Eng., 1992)

A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. - Mark E. Stickel (Theor. Comput. Sci., 1992)

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 (S&P, 1993)

Interpretation as Abduction. - Jerry R. Hobbs; Mark E. Stickel; Douglas E. Appelt; Paul A. Martin (Artif. Intell., 1993)

Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers. - Mark E. Stickel (Future Gener. Comput. Syst., 1993)

Deductive Composition of Astronomical Software from Subroutine Libraries. - Mark E. Stickel; Richard J. Waldinger; Michael R. Lowry; Thomas Pressburger; Ian Underwood (CADE, 1994)

Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. - Tomás E. Uribe; Mark E. Stickel (CCL, 1994)

Elimination of inference channels by optimal upgrading. - Mark E. Stickel (S&P, 1994)

Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction. - Mark E. Stickel (J. Autom. Reason., 1994)

Term Rewriting in Contemporary Resolution Theorem Proving (Abstract). - Mark E. Stickel (RTA, 1995)

Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results. - Mark E. Stickel; Hantao Zhang 001 (RTA, 1995)

SRI's Tipster II Project. - Jerry R. Hobbs; Douglas E. Appelt; John Bear; David J. Israel; Megumi Kameyama; Andrew Kehler; Mark E. Stickel; Mabry Tyson (TIPSTER, 1996)

A Practical Integration of First-Order Reasoning and Decision Procedures. - Nikolaj S. Bjørner; Mark E. Stickel; Tomás E. Uribe (CADE, 1997)

FASTUS: A Cascaded Finite-State Transducer for Extracting Information from Natural-Language Text - Jerry R. Hobbs; Douglas E. Appelt; John Bear; David J. Israel; Megumi Kameyama; Mark E. Stickel; Mabry Tyson (CoRR, 1997)

Using Prior Knowledge: Problems and Solutions. - Vinay K. Chaudhri; Mark E. Stickel; Jérôme Thoméré; Richard J. Waldinger (AAAI/IAAI, 2000)

Implementing the Davis-Putnam Method. - Hantao Zhang 001; Mark E. Stickel (J. Autom. Reason., 2000)

Balance and Filtering in Structured Satisfiable Problems. - Henry A. Kautz; Yongshao Ruan; Dimitris Achlioptas; Carla P. Gomes; Bart Selman; Mark E. Stickel (IJCAI, 2001)

Balance and Filtering in Structured Satisfiable Problems (Preliminary Report). - Henry A. Kautz; Yongshao Ruan; Dimitris Achlioptas; Carla P. Gomes; Bart Selman; Mark E. Stickel (Electron. Notes Discret. Math., 2001)

Deductive Question Answering from Multiple Resources. - Richard J. Waldinger; Douglas E. Appelt; Jennifer L. Dungan; John Fry; Jerry R. Hobbs; David J. Israel; Peter Jarvis; David L. Martin 001; Susanne Z. Riehemann; Mark E. Stickel; Mabry Tyson (New Directions in Question Answering, 2004)

Building Theorem Provers. - Mark E. Stickel (CADE, 2009)