William McCune

Publication Activity (10 Years)

Years Active: 1982-2006
Publications (10 Years): 0

Publications

William McCune
Semantic Guidance for Saturation Provers. AISC (2006)
Olga Shumsky Matlin, William McCune
Encapsulation for Practical Simplification Procedures CoRR (2004)
Olga Shumsky Matlin, William McCune, Ewing L. Lusk
Methods to Model-Check Parallel Systems Software CoRR (2003)
William McCune
Mace4 Reference Manual and Guide CoRR (2003)
William McCune
OTTER 3.3 Reference Manual CoRR (2003)
William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos
Short Single Axioms for Boolean Algebra. J. Autom. Reason. 29 (1) (2002)
Olga Shumsky Matlin, Ewing L. Lusk, William McCune
SPINning Parallel Systems Software. SPIN (2002)
Olga Shumsky Matlin, Ewing L. Lusk, William McCune
SPINning Parallel Systems Software CoRR (2002)
William McCune
MACE 2.0 Reference Manual and Guide CoRR (2001)
William McCune, Olga Shumsky
System Description: IVY. CADE (2000)
William McCune
Automatic Proofs and Counterexamples for Some Ortholattice Identities. Inf. Process. Lett. 65 (6) (1998)
Olga Shumsky, Ralph W. Wilkerson, William McCune, Fikret Erçal
Direct finite first-order model generation with negative constraint propagation heuristic. SAC (1997)
William McCune
Solution of the Robbins Problem. J. Autom. Reason. 19 (3) (1997)
William McCune, Larry Wos
Otter - The CADE-13 Competition Incarnations. J. Autom. Reason. 18 (2) (1997)
William McCune
Well-Behaved Search and the Robbins Problem. RTA (1997)
Maria Paola Bonacina, William McCune
Distributed Theorem Proving by Peers. CADE (1994)
John K. Slaney, Ewing L. Lusk, William McCune
SCOTT: Semantically Constrained Otter System Description. CADE (1994)
William McCune
Single Axioms for the Left Group and the Right Group Calculi. Notre Dame J. Formal Log. 34 (1) (1993)
William McCune
Single Axioms for Groups and Abelian Groups with Various Operations. J. Autom. Reason. 10 (1) (1993)
Ewing L. Lusk, William McCune
Uniform Strategies: The CADE-11 Theorem Proving Contest. J. Autom. Reason. 11 (3) (1993)
William McCune, Larry Wos
Experiments in Automated Deduction with Condensed Detachment. CADE (1992)
Larry Wos, William McCune
The Application of Automated Reasoning to Questions in Mathematics and Logic. Ann. Math. Artif. Intell. 5 (2-4) (1992)
Ewing L. Lusk, William McCune, John K. Slaney
ROO: A Parallel Theorem Prover. CADE (1992)
William McCune, Larry Wos
Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. LPAR (1992)
William McCune
Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. J. Autom. Reason. 9 (1) (1992)
William McCune
Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. J. Autom. Reason. 9 (2) (1992)
Larry Wos, William McCune
Automated Theorem Proving and Logic Programming. J. Log. Program. 11 (1&2) (1991)
William McCune, Larry Wos
The Absence and the Presence of Fixed Point Combinators. Theor. Comput. Sci. 87 (1) (1991)
William McCune
Skolem Functions and Equality in Automated Deduction. AAAI (1990)
Ewing L. Lusk, William McCune, John K. Slaney
Parallel Closure-Based Automated Reasoning. Dagstuhl Seminar on Parallelization in Inference Systems (1990)
Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler
Automated Reasoning Contributed to Mathematics and Logic. CADE (1990)
Ewing L. Lusk, William McCune
Tutorial on High-Performance Automated Theorem Proving. CADE (1990)
William McCune
OTTER 2.0. CADE (1990)
Ewing L. Lusk, William McCune
Experiments with ROO: A Parallel Automated Deduction System. Dagstuhl Seminar on Parallelization in Inference Systems (1990)
Cynthia A. Wick, William McCune
Automated Reasoning about Elementary Point-Set Topology. J. Autom. Reason. 5 (2) (1989)
William McCune, Lawrence J. Henschen
Maintaining state constraints in relational databases: a proof theoretic basis. J. ACM 36 (1) (1989)
William McCune
Challenge Equality Problems in Lattice Theory. CADE (1988)
Larry Wos, William McCune
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. CADE (1988)
William McCune
Un-Skolemizing Clause Sets. Inf. Process. Lett. 29 (5) (1988)
William McCune, Larry Wos
A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic. J. Autom. Reason. 3 (1) (1987)
Ewing L. Lusk, William McCune, Ross A. Overbeek
ITP at Argonne National Laboratory. CADE (1986)
Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek
Parallel Logic Programming for Numeric Applications. ICLP (1986)
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. Reason. 2 (3) (1986)
Larry Wos, William McCune
Negative Paramodulation. CADE (1986)
Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek
Paths to High-Performance Automated Theorem Proving. CADE (1986)
William McCune, Lawrence J. Henschen
Experiments with Semantic Paramodulation. J. Autom. Reason. 1 (3) (1985)
Larry Wos, Robert Veroff, Barry Smith, William McCune
The Linked Inference Principle, II: The User's Viewpoint. CADE (1984)
William McCune, Lawrence J. Henschen
Semantic Paramodulation for Horn Sets. IJCAI (1983)
Lawrence J. Henschen, William McCune, Shamim A. Naqvi
Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory (1982)
Ewing L. Lusk, William McCune, Ross A. Overbeek
Logic Machine Architecture: Inference Mechanisms. CADE (1982)
Ewing L. Lusk, William McCune, Ross A. Overbeek
Logic Machine Architecture: Kernel Funtions. CADE (1982)