Compiling Constraint-Checking Programs from First-Order Formulas. - Lawrence J. Henschen; William McCune; Shamim A. Naqvi (Advances in Data Base Theory, 1982)

Logic Machine Architecture: Kernel Funtions. - Ewing L. Lusk; William McCune; Ross A. Overbeek (CADE, 1982)

Logic Machine Architecture: Inference Mechanisms. - Ewing L. Lusk; William McCune; Ross A. Overbeek (CADE, 1982)

Semantic Paramodulation for Horn Sets. - William McCune; Lawrence J. Henschen (IJCAI, 1983)

The Linked Inference Principle, II: The User's Viewpoint. - Larry Wos; Robert Veroff; Barry Smith 002; William McCune (CADE, 1984)

Experiments with Semantic Paramodulation. - William McCune; Lawrence J. Henschen (J. Autom. Reason., 1985)

Paths to High-Performance Automated Theorem Proving. - Ralph Butler; Ewing L. Lusk; William McCune; Ross A. Overbeek (CADE, 1986)

ITP at Argonne National Laboratory. - Ewing L. Lusk; William McCune; Ross A. Overbeek (CADE, 1986)

Negative Paramodulation. - Larry Wos; William McCune (CADE, 1986)

Parallel Logic Programming for Numeric Applications. - Ralph Butler; Ewing L. Lusk; William McCune; Ross A. Overbeek (ICLP, 1986)

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)

A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. - William McCune; Larry Wos (J. Autom. Reason., 1987)

Challenge Equality Problems in Lattice Theory. - William McCune (CADE, 1988)

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. - Larry Wos; William McCune (CADE, 1988)

Un-Skolemizing Clause Sets. - William McCune (Inf. Process. Lett., 1988)

Maintaining state constraints in relational databases: a proof theoretic basis. - William McCune; Lawrence J. Henschen (J. ACM, 1989)

Automated Reasoning about Elementary Point-Set Topology. - Cynthia A. Wick; William McCune (J. Autom. Reason., 1989)

Skolem Functions and Equality in Automated Deduction. - William McCune (AAAI, 1990)

Tutorial on High-Performance Automated Theorem Proving. - Ewing L. Lusk; William McCune (CADE, 1990)

OTTER 2.0. - William McCune (CADE, 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 (CADE, 1990)

Experiments with ROO: A Parallel Automated Deduction System. - Ewing L. Lusk; William McCune (Dagstuhl Seminar on Parallelization in Inference Systems, 1990)

Parallel Closure-Based Automated Reasoning. - Ewing L. Lusk; William McCune; John K. Slaney (Dagstuhl Seminar on Parallelization in Inference Systems, 1990)

Automated Theorem Proving and Logic Programming. - Larry Wos; William McCune (J. Log. Program., 1991)

The Absence and the Presence of Fixed Point Combinators. - William McCune; Larry Wos (Theor. Comput. Sci., 1991)

ROO: A Parallel Theorem Prover. - Ewing L. Lusk; William McCune; John K. Slaney (CADE, 1992)

Experiments in Automated Deduction with Condensed Detachment. - William McCune; Larry Wos (CADE, 1992)

Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. - William McCune; Larry Wos (LPAR, 1992)

The Application of Automated Reasoning to Questions in Mathematics and Logic. - Larry Wos; William McCune (Ann. Math. Artif. Intell., 1992)

Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. - William McCune (J. Autom. Reason., 1992)

Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. - William McCune (J. Autom. Reason., 1992)

Uniform Strategies: The CADE-11 Theorem Proving Contest. - Ewing L. Lusk; William McCune (J. Autom. Reason., 1993)

Single Axioms for Groups and Abelian Groups with Various Operations. - William McCune (J. Autom. Reason., 1993)

Single Axioms for the Left Group and the Right Group Calculi. - William McCune (Notre Dame J. Formal Log., 1993)

Distributed Theorem Proving by Peers. - Maria Paola Bonacina; William McCune (CADE, 1994)

SCOTT: Semantically Constrained Otter System Description. - John K. Slaney; Ewing L. Lusk; William McCune (CADE, 1994)

Automated Deduction in Equational Logic and Cubic Curves - William McCune; R. Padmanabhan (Springer, 1996)

Well-Behaved Search and the Robbins Problem. - William McCune (RTA, 1997)

Direct finite first-order model generation with negative constraint propagation heuristic. - Olga Shumsky; Ralph W. Wilkerson; William McCune; Fikret Erçal (SAC, 1997)

Solution of the Robbins Problem. - William McCune (J. Autom. Reason., 1997)

Otter - The CADE-13 Competition Incarnations. - William McCune; Larry Wos (J. Autom. Reason., 1997)

Automatic Proofs and Counterexamples for Some Ortholattice Identities. - William McCune (Inf. Process. Lett., 1998)

System Description: IVY. - William McCune; Olga Shumsky (CADE, 2000)

MACE 2.0 Reference Manual and Guide - William McCune (CoRR, 2001)

SPINning Parallel Systems Software. - Olga Shumsky Matlin; Ewing L. Lusk; William McCune (SPIN, 2002)

Short Single Axioms for Boolean Algebra. - William McCune; Robert Veroff; Branden Fitelson; Kenneth Harris; Andrew Feist; Larry Wos (J. Autom. Reason., 2002)

Methods to Model-Check Parallel Systems Software - Olga Shumsky Matlin; William McCune; Ewing L. Lusk (CoRR, 2003)

Mace4 Reference Manual and Guide - William McCune (CoRR, 2003)

OTTER 3.3 Reference Manual - William McCune (CoRR, 2003)

Encapsulation for Practical Simplification Procedures - Olga Shumsky Matlin; William McCune (CoRR, 2004)

Semantic Guidance for Saturation Provers. - William McCune (AISC, 2006)

Otter/Ivy. - Michael Beeson; William McCune (The Seventeen Provers of the World, 2006)