| 2006 | AISC | Semantic Guidance for Saturation Provers. | William McCune |
| 2000 | CADE | System Description: IVY. | William McCune, Olga Shumsky |
| 1997 | SAC | Direct finite first-order model generation with negative constraint propagation heuristic. | Olga Shumsky, Ralph W. Wilkerson, William McCune, Fikret Eral |
| 1994 | CADE | Distributed Theorem Proving by Peers. | Maria Paola Bonacina, William McCune |
| 1994 | CADE | SCOTT: Semantically Constrained Otter System Description. | John K. Slaney, Ewing L. Lusk, William McCune |
| 1992 | CADE | ROO: A Parallel Theorem Prover. | Ewing L. Lusk, William McCune, John K. Slaney |
| 1992 | CADE | Experiments in Automated Deduction with Condensed Detachment. | William McCune, Larry Wos |
| 1992 | LPAR | Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. | William McCune, Larry Wos |
| 1990 | AAAI | Skolem Functions and Equality in Automated Deduction. | William McCune |
| 1990 | CADE | Tutorial on High-Performance Automated Theorem Proving. | Ewing L. Lusk, William McCune |
| 1990 | CADE | OTTER 2.0. | William McCune |
| 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 Equality Problems in Lattice Theory. | William McCune |
| 1988 | CADE | Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. | Larry Wos, William McCune |
| 1986 | CADE | Paths to High-Performance Automated Theorem Proving. | Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1986 | CADE | ITP at Argonne National Laboratory. | Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1986 | CADE | Negative Paramodulation. | Larry Wos, William McCune |
| 1986 | ICLP | Parallel Logic Programming for Numeric Applications. | Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1984 | CADE | The Linked Inference Principle, II: The User's Viewpoint. | Larry Wos, Robert Veroff, Barry Smith, William McCune |
| 1983 | IJCAI | Semantic Paramodulation for Horn Sets. | William McCune, Lawrence J. Henschen |
| 1982 | CADE | Logic Machine Architecture: Kernel Funtions. | Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1982 | CADE | Logic Machine Architecture: Inference Mechanisms. | Ewing L. Lusk, William McCune, Ross A. Overbeek |