Updated Sep 24, 2008.
Books

W. McCune and R. Padmanabhan.
Automated Deduction in Equational Logic and Cubic Curves,
volume 1095 of Lecture Notes in Computer Science (AI subseries).
SpringerVerlag, Berlin, 1996.

W. McCune, editor.
Proceedings of the 14th International Conference on Automated
Deduction, volume 1249 of Lecture Notes in Computer Science (AI
subseries).
SpringerVerlag, Berlin, 1997.
Journal Articles and Book Chapters

L. Henschen, W. McCune, and S. Naqvi.
Compiling constraintchecking programs from firstorder formulas.
In H. Gallaire, J. Minker, and J.M. Nicolas, editors, Advances
in Database Theory, Vol. 2. Plenum Press, 1984.

W. McCune.
Experiments with semantic paramodulation.
J. Automated Reasoning, 1(3):231261, 1984.

R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos.
Set theory in firstorder logic: Clauses for Gödel's axioms.
J. Automated Reasoning, 2(3):287327, 1986.

W. McCune and L. Wos.
A case study in automated theorem proving: Searching for sages in
combinatory logic.
J. Automated Reasoning, 3(1):91107, 1987.

W. McCune.
UnSkolemizing clause sets.
Information Processing Letters, 29:257263, November 1988.

W. McCune and L. Henschen.
Maintaining state constraints in relational databases: A proof
theoretic basis.
J. ACM, 36(1):4668, 1989.

C. Wick and W. McCune.
Automated reasoning about elementary pointset topology.
J. Automated Reasoning, 5(2):239255, 1989.

L. Wos and W. McCune.
Automated theorem proving and logic programming: A natural
symbiosis.
J. Logic Programming, 11(1):153, July 1991.

W. McCune and L. Wos.
The absence and the presence of fixed point combinators.
Theoretical Computer Science, 87:221228, 1991.

W. McCune.
Experiments with discrimination tree indexing and path indexing for
term retrieval.
J. Automated Reasoning, 9(2):147167, 1992.

L. Wos and W. McCune.
The application of automated reasoning to questions in mathematics
and logic.
Annals of Mathematics and Artificial Intelligence, 5:321370,
1992.

E. Lusk and W. McCune.
Experiments with Roo, a parallel automated deduction system.
In B. Fronhöfer and G. Wrightson, editors, Parallelization
in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590,
pages 139162, Berlin, 1992. SpringerVerlag.

W. McCune.
Automated discovery of new axiomatizations of the left group and
right group calculi.
J. Automated Reasoning, 9(1):124, 1992.

W. McCune.
Single axioms for the left group and right group calculi.
Notre Dame J. Formal Logic, 34(1):132139, 1993.

W. McCune.
Single axioms for groups and Abelian groups with various
operations.
J. Automated Reasoning, 10(1):113, 1993.

E. L. Lusk and W. McCune.
Uniform strategies: The CADE11 theorem proving contest.
J. Automated Reasoning, 11(3):317331, 1993.

R. Padmanabhan and W. McCune.
Single identities for ternary Boolean algebras.
Computers and Mathematics with Applications, 29(2):1316,
1995.

R. Padmanabhan and W. McCune.
Automated reasoning about cubic curves.
Computers and Mathematics with Applications, 29(2):1726,
1995.

W. McCune and R. Padmanabhan.
Single identities for lattice theory and for weakly associative
lattices.
Algebra Universalis, 36(4):436449, 1996.

W. McCune and A. D. Sands.
Computer and human reasoning: Single implicative axioms for groups
and for Abelian groups.
American Mathematical Monthly, 103(10):888892, December 1996.

W. McCune and L. Wos.
Otter: The CADE13 competition incarnations.
J. Automated Reasoning, 18(2):211220, 1997.

W. McCune.
33 basic test problems: A practical evaluation of some paramodulation
strategies.
In Robert Veroff, editor, Automated Reasoning and its
Applications: Essays in Honor of Larry Wos, chapter 5, pages 71114. MIT
Press, 1997.

W. McCune.
Solution of the Robbins problem.
J. Automated Reasoning, 19(3):263276, 1997.

W. McCune.
Automatic proofs and counterexamples for some ortholattice
identities.
Information Processing Letters, 65:285291, 1998.

W. McCune and O. Shumsky.
IVY: A preprocessor and proof checker for firstorder logic.
In M. Kaufmann, P. Manolios, and J Moore, editors, \em
ComputerAided Reasoning: ACL2 Case Studies, chapter 16. Kluwer Academic,
2000.

W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist, and L. Wos.
Short single axioms for Boolean algebra.
J. Automated Reasoning, 29(1):116, 2002.

W. McCune, R. Padmanabhan, and R. Veroff.
Yet another single law for lattices.
Algebra Universalis, 50(2):165169, 2003.

W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff.
Automated discovery of single axioms for ortholattices.
Algebra Universalis, 52:541549, 2005.

R. Padmanabhan, W. McCune, and R. Veroff.
Levi's commutator theorems for cancellative semigroups.
Semigroup Forum, 71:152157, 2005.

R. Padmanabhan and W. McCune.
Uniqueness of Steiner laws on cubic curves.
Beitr\"age zur Algebra und Geometrie, 47(2):543557, 2006.

R. Padmanabhan, W. McCune, and R. Veroff.
Lattice laws forcing distributivity under unique complementation.
Houston J. Math., 33(2):391401, 2007.

W. McCune.
Some Prover9 proofs.
Appendix A in R. Padmanabhan and S. Rudeanu, Axioms for Lattices
and Boolean Algebras, pages 147158. World Scientific, 2008.
Refereed Conference Proceedings

E. Lusk, W. McCune, and R. Overbeek.
Logic Machine Architecture: Kernel functions.
In D. Loveland, editor, Proceedings of the 6th Conference on
Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages
7084, Berlin, 1982. SpringerVerlag.

E. Lusk, W. McCune, and R. Overbeek.
Logic Machine Architecture: Inference mechanisms.
In D. Loveland, editor, Proceedings of the 6th Conference on
Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages
85108, Berlin, 1982. SpringerVerlag.

W. McCune and L. Henschen.
Semantic paramodulation for Horn sets.
In A. Bundy, editor, Proceedings of the 8th International Joint
Conference on Artificial Intelligence, volume 2, pages 902908, 1983.

L. Wos, R. Veroff, B. Smith, and W. McCune.
The linked inference principle II: The user's view.
In R. Shostak, editor, Proceedings of the 7th International
Conference on Automated Deduction, Lecture Notes in Computer Science, Vol.
170, pages 316332, Berlin, 1984. SpringerVerlag.

E. Lusk, W. McCune, and R. Overbeek.
ITP at Argonne National Laboratory.
In J. Siekmann, editor, Proceedings of the 8th International
Conference on Automated Deduction, Lecture Notes in Computer Science, Vol.
230, pages 697698, Berlin, 1986. SpringerVerlag.
Extended abstract.

R. Butler, E. Lusk, W. McCune, and R. Overbeek.
Parallel logic programming for numeric applications.
In E. Shapiro, editor, Proceedings of the Third Conference on
Logic Programming, Lecture Notes in Computer Science, Vol. 225, pages
375388, Berlin, 1986. SpringerVerlag.

L. Wos and W. McCune.
Negative paramodulation.
In J. Siekmann, editor, Proceedings of the 8th International
Conference on Automated Deduction, Lecture Notes in Computer Science, Vol.
230, pages 229239, Berlin, 1986. SpringerVerlag.

R. Butler, E. Lusk, W. McCune, and R. Overbeek.
Paths to highperformance automated theorem proving.
In J. Siekmann, editor, Proceedings of the 8th International
Conference on Automated Deduction, Lecture Notes in Computer Science, Vol.
230, pages 588597, Berlin, 1986. SpringerVerlag.

L. Wos and W. McCune.
Challenge problems focusing on equality and combinatory logic:
Evaluating automated theoremproving programs.
In E. Lusk and R. Overbeek, editors, Proceedings of the 9th
International Conference on Automated Deduction, Lecture Notes in Computer
Science, Vol. 310, pages 714729, Berlin, 1988. SpringerVerlag.

W. McCune.
Challenge equality problems in lattice theory.
In E. Lusk and R. Overbeek, editors, Proceedings of the 9th
International Conference on Automated Deduction, Lecture Notes in Computer
Science, Vol. 310, pages 704709, Berlin, 1988. SpringerVerlag.

L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler.
Automated reasoning contributes to mathematics and logic.
In M. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 449, pages 485499, Berlin, 1990. SpringerVerlag.

W. McCune.
Otter 2.0.
In M. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 449, pages 663664, Berlin, 1990. SpringerVerlag.
Extended abstract.

W. McCune.
Skolem functions and equality in automated deduction.
In Proceedings of the Eighth National Conference on Artificial
Intelligence, pages 246251, Cambridge, MA, 1990. MIT Press.

W. McCune and L. Wos.
Experiments in automated deduction with condensed detachment.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 607, pages 209223, Berlin, 1992. SpringerVerlag.

E. Lusk, W. McCune, and J. Slaney.
ROO: A parallel theorem prover.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 607, pages 731734, Berlin, 1992. SpringerVerlag.
Extended abstract.

W. McCune and L. Wos.
Application of automated deduction to the search for single axioms
for exponent groups.
In A. Voronkov, editor, Logic Programming and Automated
Reasoning, LNAI Vol. 624, pages 131136, Berlin, 1992. SpringerVerlag.

M. Bonacina and W. McCune.
Distributed theorem proving by Peers.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 814, pages 841845. SpringerVerlag, 1994.
Extended abstract.

J. Slaney, E. Lusk, and W. McCune.
SCOTT: Semantically constrained Otter.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 814, pages 764768. SpringerVerlag, 1994.
Extended abstract.

W. McCune.
Wellbehaved search and the Robbins problem (extended abstract).
In H. Comon, editor, Proceedings of RTA'97, Lecture Notes in
Computer Science, Vol. 1232, pages 17. SpringerVerlag, 1997.

W. McCune and O. Shumsky.
System description: IVY.
In D. McAllester, editor, Proceedings of the 17th International
Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
Vol. 1831, pages 401405. SpringerVerlag, 2000.
Extended abstract.

E. Lusk and W. McCune.
ACL2 for parallel systems software.
In M. Kaufmann and J S. Moore, editors, ACL2 Workshop 2000
Proceedings. University of Texas at Austin, 2000.
http://www.cs.utexas.edu/us\ers/moore/acl2/workshop2000/.

W. McCune.
Single axioms: With and without computers.
In X.S. Gao and D. Wang, editors, Computer Mathematics:
Procedings of ASCM 2000, pages 8389, Singapore, 2000. World Scientific.

O. Matlin, E. Lusk, and W. McCune.
SPINning parallel systems software.
In D. Bo\usna\ucki and S. Leue, editors, Model Checking
Software. Proceedings of the 9th International SPIN Workshop, LNCS 2318,
pages 213220. Springer Verlag, 2002.

O. Matlin and W. McCune.
Encapsulation for practical simplification procedures.
In Proceedings of the ACL2 Workshop, Boulder, Colorado, July
2003.

W. McCune.
Semantic guidance for saturation provers.
In J. Calmet, T. Ida, and D. Wang, editors, Proceeding of the
8th International Conference on Artificial Intelligence and Symbolic
Computation, Lecture Notes in Artificial Intelligence, Vol. 4120, pages
1824. Springer, 2006.
Preprints and Drafts

R. Padmanabhan and W. McCune.
Tarski theorems on selfdual equational bases for groups.
Preprint ANL/MCSP10920903, Argonne National Laboratory, Argonne,
IL, August 2004.
Other Papers

L. Wos and W. McCune.
Searching for fixed point combinators by using automated theorem
proving: A preliminary report.
Tech. Report ANL88/10, Argonne National Laboratory, Argonne, IL,
September 1988.

W. McCune.
Otter 1.0 Users' Guide.
Tech. Report ANL88/44, Argonne National Laboratory, Argonne, IL,
January 1989.

A. Jindal, R. Overbeek, and W. McCune.
A parallel processing approach for implementing highperformance
firstorder logic deduction systems.
Tech. Memo ANL/MCSTM131, Argonne National Laboratory, Argonne, IL,
April 1989.

W. McCune.
Otter 2.0 Users Guide.
Tech. Report ANL90/9, Argonne National Laboratory, Argonne, IL,
March 1990.

T. Henry and W. McCune.
FormEd: An X Window System Application for Managing
Firstorder Formulas.
Tech. Memo ANL/MCSTM141, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, October 1990.

L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler.
Otter experiments pertinent to CADE10.
Tech. Report ANL89/36, Argonne National Laboratory, Argonne, IL,
1991.

E. Lusk, W. McCune, and J. Slaney.
Rooa parallel theorem prover.
Tech. Memo ANL/MCSTM149, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, 1991.

L. Wos and W. McCune.
The application of automated reasoning to proof translation and to
finding proofs with specified properties: A case study in manyvalued
sentential calculus.
Tech. Report ANL91/19, Argonne National Laboratory, Argonne, IL,
1991.

W. McCune.
What's New in Otter 2.2.
Tech. Memo ANL/MCSTM153, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, July 1991.

W. McCune.
Proofs for Group and Abelian Group Single Axioms.
Tech. Memo ANL/MCSTM156, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, October 1991.

W. McCune.
Otter 3.0 Reference Manual and Guide.
Tech. Report ANL94/6, Argonne National Laboratory, Argonne, IL,
1994.
Also see \verbhttp://www.mcs.anl.gov/AR/otter/.

W. McCune.
Otter 3.0 [data on TPTP problem set].
Preprint MCSP39991193, Argonne National Laboratory, Argonne, IL,
November 1993.

W. McCune.
A Case Study in Automated Theorem Proving: A Difficult
Problem about Commutators.
Tech. Memo. ANL/MCSTM202, Argonne National Laboratory, Argonne, IL,
1995.

W. McCune.
Single Axioms for Boolean Algebra.
Tech. Memo ANL/MCSTM243, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, June 2000.

R. Veroff and W. McCune.
A short Sheffer axiom for Boolean Algebra.
Tech. Memo ANL/MCSTM244, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, June 2000.

W. McCune.
Mace 2.0 Reference Manual and Guide.
Tech. Memo ANL/MCSTM249, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, June 2001.

W. McCune.
Otter 3.3 Reference Manual.
Tech. Memo ANL/MCSTM263, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.

W. McCune.
Mace4 Reference Manual and Guide.
Tech. Memo ANL/MCSTM264, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.

W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff.
Short equational bases for ortholattices: Proofs and countermodels.
Tech. Memo ANL/MCSTM265, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, September 2003.

O. Matlin, W. McCune, and E. Lusk.
Methods to modelcheck parallel systems software.
Tech. Memo. ANL/MCSTM261, Argonne National Laboratory, Argonne, IL,
April 2003.

W. McCune.
Fascinating XCB Inference.
Association for Automated Reasoning Newsletter, (66), February
2005.
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.