Publications of William McCune

Updated Sep 24, 2008.

Books

  1. W. McCune and R. Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves, volume 1095 of Lecture Notes in Computer Science (AI subseries). Springer-Verlag, Berlin, 1996.
  2. W. McCune, editor. Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Computer Science (AI subseries). Springer-Verlag, Berlin, 1997.

Journal Articles and Book Chapters

  1. L. Henschen, W. McCune, and S. Naqvi. Compiling constraint-checking programs from first-order formulas. In H. Gallaire, J. Minker, and J.-M. Nicolas, editors, Advances in Database Theory, Vol. 2. Plenum Press, 1984.
  2. W. McCune. Experiments with semantic paramodulation. J. Automated Reasoning, 1(3):231--261, 1984.
  3. R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first-order logic: Clauses for Gödel's axioms. J. Automated Reasoning, 2(3):287--327, 1986.
  4. W. McCune and L. Wos. A case study in automated theorem proving: Searching for sages in combinatory logic. J. Automated Reasoning, 3(1):91--107, 1987.
  5. W. McCune. Un-Skolemizing clause sets. Information Processing Letters, 29:257--263, November 1988.
  6. W. McCune and L. Henschen. Maintaining state constraints in relational databases: A proof theoretic basis. J. ACM, 36(1):46--68, 1989.
  7. C. Wick and W. McCune. Automated reasoning about elementary point-set topology. J. Automated Reasoning, 5(2):239--255, 1989.
  8. L. Wos and W. McCune. Automated theorem proving and logic programming: A natural symbiosis. J. Logic Programming, 11(1):1--53, July 1991.
  9. W. McCune and L. Wos. The absence and the presence of fixed point combinators. Theoretical Computer Science, 87:221--228, 1991.
  10. W. McCune. Experiments with discrimination tree indexing and path indexing for term retrieval. J. Automated Reasoning, 9(2):147--167, 1992.
  11. L. Wos and W. McCune. The application of automated reasoning to questions in mathematics and logic. Annals of Mathematics and Artificial Intelligence, 5:321--370, 1992.
  12. 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 139--162, Berlin, 1992. Springer-Verlag.
  13. W. McCune. Automated discovery of new axiomatizations of the left group and right group calculi. J. Automated Reasoning, 9(1):1--24, 1992.
  14. W. McCune. Single axioms for the left group and right group calculi. Notre Dame J. Formal Logic, 34(1):132--139, 1993.
  15. W. McCune. Single axioms for groups and Abelian groups with various operations. J. Automated Reasoning, 10(1):1--13, 1993.
  16. E. L. Lusk and W. McCune. Uniform strategies: The CADE-11 theorem proving contest. J. Automated Reasoning, 11(3):317--331, 1993.
  17. R. Padmanabhan and W. McCune. Single identities for ternary Boolean algebras. Computers and Mathematics with Applications, 29(2):13--16, 1995.
  18. R. Padmanabhan and W. McCune. Automated reasoning about cubic curves. Computers and Mathematics with Applications, 29(2):17--26, 1995.
  19. W. McCune and R. Padmanabhan. Single identities for lattice theory and for weakly associative lattices. Algebra Universalis, 36(4):436--449, 1996.
  20. W. McCune and A. D. Sands. Computer and human reasoning: Single implicative axioms for groups and for Abelian groups. American Mathematical Monthly, 103(10):888--892, December 1996.
  21. W. McCune and L. Wos. Otter: The CADE-13 competition incarnations. J. Automated Reasoning, 18(2):211--220, 1997.
  22. 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 71--114. MIT Press, 1997.
  23. W. McCune. Solution of the Robbins problem. J. Automated Reasoning, 19(3):263--276, 1997.
  24. W. McCune. Automatic proofs and counterexamples for some ortholattice identities. Information Processing Letters, 65:285--291, 1998.
  25. W. McCune and O. Shumsky. IVY: A preprocessor and proof checker for first-order logic. In M. Kaufmann, P. Manolios, and J Moore, editors, \em Computer-Aided Reasoning: ACL2 Case Studies, chapter 16. Kluwer Academic, 2000.
  26. W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist, and L. Wos. Short single axioms for Boolean algebra. J. Automated Reasoning, 29(1):1--16, 2002.
  27. W. McCune, R. Padmanabhan, and R. Veroff. Yet another single law for lattices. Algebra Universalis, 50(2):165--169, 2003.
  28. W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Automated discovery of single axioms for ortholattices. Algebra Universalis, 52:541--549, 2005.
  29. R. Padmanabhan, W. McCune, and R. Veroff. Levi's commutator theorems for cancellative semigroups. Semigroup Forum, 71:152--157, 2005.
  30. R. Padmanabhan and W. McCune. Uniqueness of Steiner laws on cubic curves. Beitr\"age zur Algebra und Geometrie, 47(2):543--557, 2006.
  31. R. Padmanabhan, W. McCune, and R. Veroff. Lattice laws forcing distributivity under unique complementation. Houston J. Math., 33(2):391--401, 2007.
  32. W. McCune. Some Prover9 proofs. Appendix A in R. Padmanabhan and S. Rudeanu, Axioms for Lattices and Boolean Algebras, pages 147--158. World Scientific, 2008.

Refereed Conference Proceedings

  1. 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 70--84, Berlin, 1982. Springer-Verlag.
  2. 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 85--108, Berlin, 1982. Springer-Verlag.
  3. 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 902--908, 1983.
  4. 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 316--332, Berlin, 1984. Springer-Verlag.
  5. 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 697--698, Berlin, 1986. Springer-Verlag. Extended abstract.
  6. 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 375--388, Berlin, 1986. Springer-Verlag.
  7. 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 229--239, Berlin, 1986. Springer-Verlag.
  8. R. Butler, E. Lusk, W. McCune, and R. Overbeek. Paths to high-performance automated theorem proving. In J. Siekmann, editor, Proceedings of the 8th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 230, pages 588--597, Berlin, 1986. Springer-Verlag.
  9. L. Wos and W. McCune. Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving 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 714--729, Berlin, 1988. Springer-Verlag.
  10. 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 704--709, Berlin, 1988. Springer-Verlag.
  11. 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 485--499, Berlin, 1990. Springer-Verlag.
  12. 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 663--664, Berlin, 1990. Springer-Verlag. Extended abstract.
  13. W. McCune. Skolem functions and equality in automated deduction. In Proceedings of the Eighth National Conference on Artificial Intelligence, pages 246--251, Cambridge, MA, 1990. MIT Press.
  14. 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 209--223, Berlin, 1992. Springer-Verlag.
  15. 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 731--734, Berlin, 1992. Springer-Verlag. Extended abstract.
  16. 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 131--136, Berlin, 1992. Springer-Verlag.
  17. 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 841--845. Springer-Verlag, 1994. Extended abstract.
  18. 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 764--768. Springer-Verlag, 1994. Extended abstract.
  19. W. McCune. Well-behaved search and the Robbins problem (extended abstract). In H. Comon, editor, Proceedings of RTA'97, Lecture Notes in Computer Science, Vol. 1232, pages 1--7. Springer-Verlag, 1997.
  20. 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 401--405. Springer-Verlag, 2000. Extended abstract.
  21. 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/workshop-2000/.
  22. W. McCune. Single axioms: With and without computers. In X.-S. Gao and D. Wang, editors, Computer Mathematics: Procedings of ASCM 2000, pages 83--89, Singapore, 2000. World Scientific.
  23. 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 213--220. Springer Verlag, 2002.
  24. O. Matlin and W. McCune. Encapsulation for practical simplification procedures. In Proceedings of the ACL2 Workshop, Boulder, Colorado, July 2003.
  25. 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 18--24. Springer, 2006.

Preprints and Drafts

  1. R. Padmanabhan and W. McCune. Tarski theorems on self-dual equational bases for groups. Preprint ANL/MCS-P1092-0903, Argonne National Laboratory, Argonne, IL, August 2004.

Other Papers

  1. L. Wos and W. McCune. Searching for fixed point combinators by using automated theorem proving: A preliminary report. Tech. Report ANL-88/10, Argonne National Laboratory, Argonne, IL, September 1988.
  2. W. McCune. Otter 1.0 Users' Guide. Tech. Report ANL-88/44, Argonne National Laboratory, Argonne, IL, January 1989.
  3. A. Jindal, R. Overbeek, and W. McCune. A parallel processing approach for implementing high-performance first-order logic deduction systems. Tech. Memo ANL/MCS-TM-131, Argonne National Laboratory, Argonne, IL, April 1989.
  4. W. McCune. Otter 2.0 Users Guide. Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, IL, March 1990.
  5. T. Henry and W. McCune. FormEd: An X Window System Application for Managing First-order Formulas. Tech. Memo ANL/MCS-TM-141, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, October 1990.
  6. L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler. Otter experiments pertinent to CADE-10. Tech. Report ANL-89/36, Argonne National Laboratory, Argonne, IL, 1991.
  7. E. Lusk, W. McCune, and J. Slaney. Roo---a parallel theorem prover. Tech. Memo ANL/MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
  8. L. Wos and W. McCune. The application of automated reasoning to proof translation and to finding proofs with specified properties: A case study in many-valued sentential calculus. Tech. Report ANL-91/19, Argonne National Laboratory, Argonne, IL, 1991.
  9. W. McCune. What's New in Otter 2.2. Tech. Memo ANL/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, July 1991.
  10. W. McCune. Proofs for Group and Abelian Group Single Axioms. Tech. Memo ANL/MCS-TM-156, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, October 1991.
  11. W. McCune. Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994. Also see \verb|http://www.mcs.anl.gov/AR/otter/|.
  12. W. McCune. Otter 3.0 [data on TPTP problem set]. Preprint MCS-P3999-1193, Argonne National Laboratory, Argonne, IL, November 1993.
  13. W. McCune. A Case Study in Automated Theorem Proving: A Difficult Problem about Commutators. Tech. Memo. ANL/MCS-TM-202, Argonne National Laboratory, Argonne, IL, 1995.
  14. W. McCune. Single Axioms for Boolean Algebra. Tech. Memo ANL/MCS-TM-243, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, June 2000.
  15. R. Veroff and W. McCune. A short Sheffer axiom for Boolean Algebra. Tech. Memo ANL/MCS-TM-244, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, June 2000.
  16. W. McCune. Mace 2.0 Reference Manual and Guide. Tech. Memo ANL/MCS-TM-249, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, June 2001.
  17. W. McCune. Otter 3.3 Reference Manual. Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.
  18. W. McCune. Mace4 Reference Manual and Guide. Tech. Memo ANL/MCS-TM-264, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.
  19. W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Short equational bases for ortholattices: Proofs and countermodels. Tech. Memo ANL/MCS-TM-265, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, September 2003.
  20. O. Matlin, W. McCune, and E. Lusk. Methods to model-check parallel systems software. Tech. Memo. ANL/MCS-TM-261, Argonne National Laboratory, Argonne, IL, April 2003.
  21. 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.