| 1992 | An Interval-based Temporal Logic in a Multivalued Setting. | Mathias Bauer |
| 1992 | Difference Matching. | David A. Basin, Toby Walsh |
| 1992 | The GAZER Theorem Prover. | Dave Barker-Plummer, Alex Rothenberg |
| 1992 | &: Automated Natural Deduction. | Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill |
| 1992 | Basic Paramodulation and Superposition. | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder |
| 1992 | Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. | Franz Baader, Klaus U. Schulz |
| 1992 | Caching and Lemmaizing in Model Elimination Theorem Provers. | Owen L. Astrachan, Mark E. Stickel |
| 1992 | The SHUNYATA System. | Kurt Ammon |
| 1992 | Automatic Proofs in Mathematical Logic and Analysis. | Kurt Ammon |
| 1992 | Proving Equality Theorems with Hyper-Linking. | Geoffrey D. Alexander, David A. Plaisted |
| 1990 | Automated Reasoning Contributed to Mathematics and Logic. | Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler |
| 1990 | ACE: The Abstract Clause Engine. | David A. Wolfram |
| 1990 | Tutorial on Program-Synthetic Deduction. | Richard J. Waldinger |
| 1990 | Case-Free Programs: An Abstraction of Definite Horn Programs. | Toshiro Wakayama, T. H. Payne |
| 1990 | LISS - The Logic Inference Search System. | Andrei Voronkov |
| 1990 | Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. | Heikki Tuominen |
| 1990 | Minimizing the Number of Clauses by Renaming. | Thierry Boy de la Tour |
| 1990 | An Examination of the Prolog Technology Theorem-Prover. | Mark Tarver |
| 1990 | Automatic Acquisition of Search Guiding Heuristics. | Christian B. Suttner, Wolfgang Ertel |
| 1990 | A General Clause Theorem Prover. | Geoff Sutcliffe |
| 1990 | A Prolog Technology Theorem Prover. | Mark E. Stickel |
| 1990 | Improving Assoviative Path Orderings. | Joachim Steinbach |
| 1990 | Higher Order E-Unification. | Wayne Snyder |
| 1990 | Parallelizing the Closure Computation in Automated Deduction. | John K. Slaney, Ewing L. Lusk |
| 1990 | A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic. | Camilla Schwind |