| 2014 | CADE | OTTER Proofs in Tarskian Geometry. | Michael Beeson, Larry Wos |
| 1992 | CADE | Benchmark Problems in Which Equality Plays the Major Role. | Ewing L. Lusk, Larry Wos |
| 1992 | CADE | Experiments in Automated Deduction with Condensed Detachment. | William McCune, Larry Wos |
| 1992 | CADE | The Impossibility of the Automation of Logical Reasoning. | Larry Wos |
| 1992 | LPAR | Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. | William McCune, Larry Wos |
| 1990 | CADE | Automated Reasoning Contributed to Mathematics and Logic. | Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler |
| 1988 | CADE | Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. | Larry Wos, William McCune |
| 1986 | CADE | Negative Paramodulation. | Larry Wos, William McCune |
| 1984 | CADE | The Linked Inference Principle, II: The User's Viewpoint. | Larry Wos, Robert Veroff, Barry Smith, William McCune |
| 1983 | IJCAI | Automated Reasoning: Real Uses and Potential Uses. | Larry Wos |
| 1982 | CADE | Procedure Implementation Through Demodulation and Related Tricks. | Steven K. Winker, Larry Wos |
| 1982 | CADE | Solving Open Questions with an Automated Theorem-Proving Program. | Larry Wos |
| 1980 | CADE | Hyperparamodulation: A Refinement of Paramodulation. | Larry Wos, Ross A. Overbeek, Lawrence J. Henschen |