| 1990 | Unification in a Combination of Equational Theories: an Efficient Algorithm. | Alexandre Boudet |
| 1990 | Perspectives on Automated Deduction (Abstract). | Wolfgang Bibel |
| 1990 | Simultaneous Paramodulation. | Dan Benanav |
| 1990 | Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete. | David A. Basin |
| 1990 | Generalized Well-founded Semantics for Logic Programs (Extended Abstract). | Chitta Baral, Jorge Lobo, Jack Minker |
| 1990 | On Restrictions of Ordered Paramodulation with Simplification. | Leo Bachmair, Harald Ganzinger |
| 1990 | Rewrite Systems for Varieties of Semigroups. | Franz Baader |
| 1990 | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning |
| 1990 | A Mechanically Assisted Constructive Proof in Category Theory. | James A. Altucher, Prakash Panangaden |
| 1988 | A Mechanizable Induction Principle for Equational Specifications. | Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy |
| 1988 | First-Order Theorem Proving Using Conditional Rewrite Rules. | Hantao Zhang, Deepak Kapur |
| 1988 | Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. | Larry Wos, William McCune |
| 1988 | Elements of Z-Module Reasoning. | Tie-Cheng Wang |
| 1988 | Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. | Christoph Walther |
| 1988 | Case Inference in Resolution-Based Languages. | Toshiro Wakayama, T. H. Payne |
| 1988 | Optimal Time Bounds for Parallel Term Matching. | Rakesh M. Verma, I. V. Ramakrishnan |
| 1988 | Some Tools for an Inference Laboratory (ATINF). | Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade |
| 1988 | QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems. | V. S. Subrahmanian, Zerksis D. Umrigar |
| 1988 | Query Processing in Quantitative Logic Programming. | V. S. Subrahmanian |
| 1988 | A Prolog Technology Theorem Prover. | Mark E. Stickel |
| 1988 | The KLAUS Automated Deduction System. | Mark E. Stickel |
| 1988 | Challenge Problems from Nonassociative Rings for Theorem Provers. | Rick L. Stevens |
| 1988 | A Subsumption Algorithm Based on Characteristic Matrices. | Rolf Socher |
| 1988 | An nH-Prolog Implementation. | Bruce T. Smith, Donald W. Loveland |
| 1988 | Checking Natural Language Proofs. | Donald Simon |