William McCune

	2006
54		William McCune: Semantic Guidance for Saturation Provers. AISC 2006: 18-24
53		Michael Beeson, William McCune: Otter/Ivy. The Seventeen Provers of the World 2006: 36-40
	2004
52		Olga Shumsky Matlin, William McCune: Encapsulation for Practical Simplification Procedures CoRR cs.LO/0402010: (2004)
	2003
51		Olga Shumsky Matlin, William McCune, Ewing L. Lusk: Methods to Model-Check Parallel Systems Software CoRR cs.LO/0312012: (2003)
50		William McCune: Mace4 Reference Manual and Guide CoRR cs.SC/0310055: (2003)
49		William McCune: OTTER 3.3 Reference Manual CoRR cs.SC/0310056: (2003)
	2002
48		Olga Shumsky Matlin, Ewing L. Lusk, William McCune: SPINning Parallel Systems Software. SPIN 2002: 213-220
47		Olga Shumsky Matlin, Ewing L. Lusk, William McCune: SPINning Parallel Systems Software CoRR cs.LO/0203009: (2002)
46		William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos: Short Single Axioms for Boolean Algebra. J. Autom. Reasoning 29(1): 1-16 (2002)
	2001
45		William McCune: MACE 2.0 Reference Manual and Guide CoRR cs.LO/0106042: (2001)
	2000
44		William McCune, Olga Shumsky: System Description: IVY. CADE 2000: 401-405
	1998
43		William McCune: Automatic Proofs and Counterexamples for Some Ortholattice Identities. Inf. Process. Lett. 65(6): 285-291 (1998)
	1997
42		William McCune: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings Springer 1997
41		William McCune: Well-Behaved Search and the Robbins Problem. RTA 1997: 1-7
40		Olga Shumsky, Ralph W. Wilkerson, William McCune, Fikret Erçal: Direct finite first-order model generation with negative constraint propagation heuristic. SAC 1997: 25-29
39		William McCune, Larry Wos: Otter - The CADE-13 Competition Incarnations. J. Autom. Reasoning 18(2): 211-220 (1997)
38		William McCune: Solution of the Robbins Problem. J. Autom. Reasoning 19(3): 263-276 (1997)
	1996
37		William McCune, R. Padmanabhan: Automated Deduction in Equational Logic and Cubic Curves Springer 1996
	1994
36		John K. Slaney, Ewing L. Lusk, William McCune: SCOTT: Semantically Constrained Otter System Description. CADE 1994: 764-768
35		Maria Paola Bonacina, William McCune: Distributed Theorem Proving by Peers. CADE 1994: 841-845
	1993
34		William McCune: Single Axioms for Groups and Abelian Groups with Various Operations. J. Autom. Reasoning 10(1): 1-13 (1993)
33		Ewing L. Lusk, William McCune: Uniform Strategies: The CADE-11 Theorem Proving Contest. J. Autom. Reasoning 11(3): 317-331 (1993)
32		William McCune: Single Axioms for the Left Group and the Right Group Calculi. Notre Dame Journal of Formal Logic 34(1): 132-139 (1993)
	1992
31		William McCune, Larry Wos: Experiments in Automated Deduction with Condensed Detachment. CADE 1992: 209-223
30		Ewing L. Lusk, William McCune, John K. Slaney: ROO: A Parallel Theorem Prover. CADE 1992: 731-734
29		William McCune, Larry Wos: Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. LPAR 1992: 131-136
28		Larry Wos, William McCune: The Application of Automated Reasoning to Questions in Mathematics and Logic. Ann. Math. Artif. Intell. 5(2-4): 321-369 (1992)
27		William McCune: Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. J. Autom. Reasoning 9(1): 1-24 (1992)
26		William McCune: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. J. Autom. Reasoning 9(2): 147-167 (1992)
	1991
25		Larry Wos, William McCune: Automated Theorem Proving and Logic Programming. J. Log. Program. 11(1&2): 1-53 (1991)
24		William McCune, Larry Wos: The Absence and the Presence of Fixed Point Combinators. Theor. Comput. Sci. 87(1): 221-228 (1991)
	1990
23		William McCune: Skolem Functions and Equality in Automated Deduction. AAAI 1990: 246-251
22		Larry Wos, S. Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler: Automated Reasoning Contributed to Mathematics and Logic. CADE 1990: 485-499
21		William McCune: OTTER 2.0. CADE 1990: 663-664
20		Ewing L. Lusk, William McCune: Tutorial on High-Performance Automated Theorem Proving. CADE 1990: 681
19		Ewing L. Lusk, William McCune: Experiments with ROO: A Parallel Automated Deduction System. Dagstuhl Seminar on Parallelization in Inference Systems 1990: 139-162
18		Ewing L. Lusk, William McCune, John K. Slaney: Parallel Closure-Based Automated Reasoning. Dagstuhl Seminar on Parallelization in Inference Systems 1990: 347
	1989
17		William McCune, Lawrence J. Henschen: Maintaining state constraints in relational databases: a proof theoretic basis. J. ACM 36(1): 46-68 (1989)
16		Cynthia A. Wick, William McCune: Automated Reasoning about Elementary Point-Set Topology. J. Autom. Reasoning 5(2): 239-255 (1989)
	1988
15		William McCune: Challenge Equality Problems in Lattice Theory. CADE 1988: 704-709
14		Larry Wos, William McCune: Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. CADE 1988: 714-729
13		William McCune: Un-Skolemizing Clause Sets. Inf. Process. Lett. 29(5): 257-263 (1988)
	1987
12		William McCune, Larry Wos: A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. J. Autom. Reasoning 3(1): 91-107 (1987)
	1986
11		Larry Wos, William McCune: Negative Paramodulation. CADE 1986: 229-239
10		Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek: Paths to High-Performance Automated Theorem Proving. CADE 1986: 588-597
9		Ewing L. Lusk, William McCune, Ross A. Overbeek: ITP at Argonne National Laboratory. CADE 1986: 697-698
8		Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek: Parallel Logic Programming for Numeric Applications. ICLP 1986: 375-388
7		Robert S. Boyer, Ewing L. Lusk, William McCune, Ross A. Overbeek, Mark E. Stickel, Larry Wos: Set Theory in First-Order Logic: Clauses for Gödel's Axioms. J. Autom. Reasoning 2(3): 287-327 (1986)
	1985
6		William McCune, Lawrence J. Henschen: Experiments with Semantic Paramodulation. J. Autom. Reasoning 1(3): 231-261 (1985)
	1984
5		Larry Wos, Robert Veroff, B. Smith, William McCune: The Linked Inference Principle, II: The User's Viewpoint. CADE 1984: 316-332
	1983
4		William McCune, Lawrence J. Henschen: Semantic Paramodula tion for Horn Sets. IJCAI 1983: 902-908
	1982
3		Lawrence J. Henschen, William McCune, Shamim A. Naqvi: Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory 1982: 145-169
2		Ewing L. Lusk, William McCune, Ross A. Overbeek: Logic Machine Architecture: Kernel Funtions. CADE 1982: 70-84
1		Ewing L. Lusk, William McCune, Ross A. Overbeek: Logic Machine Architecture: Inference Mechanisms. CADE 1982: 85-108

Coauthor Index

1	Michael Beeson	[53]
2	Maria Paola Bonacina	[35]
3	Robert S. Boyer	[7]
4	Ralph M. Butler (Ralph Butler)	[8] [10] [22]
5	Fikret Erçal	[40]
6	Andrew Feist	[46]
7	Branden Fitelson	[46]
8	Kenneth Harris	[46]
9	Lawrence J. Henschen	[3] [4] [6] [17]
10	Ewing L. Lusk	[1] [2] [7] [8] [9] [10] [18] [19] [20] [22] [30] [33] [36] [47] [48] [51]
11	Olga Shumsky Matlin	[47] [48] [51] [52]
12	Shamim A. Naqvi	[3]
13	Ross A. Overbeek	[1] [2] [7] [8] [9] [10] [22]
14	R. Padmanabhan	[37]
15	Olga Shumsky	[40] [44]
16	John K. Slaney	[18] [30] [36]
17	B. Smith	[5]
18	Rick L. Stevens (Rick Stevens)	[22]
19	Mark E. Stickel	[7]
20	Robert Veroff	[5] [46]
21	Cynthia A. Wick	[16]
22	Ralph W. Wilkerson	[40]
23	S. Winker	[22]
24	Larry Wos	[5] [7] [11] [12] [14] [22] [24] [25] [28] [29] [31] [39] [46]

Colors in the list of coauthors