| 2006 |
|---|
| 54 | EE | William McCune:
Semantic Guidance for Saturation Provers.
AISC 2006: 18-24 |
| 53 | EE | Michael Beeson,
William McCune:
Otter/Ivy.
The Seventeen Provers of the World 2006: 36-40 |
| 2004 |
|---|
| 52 | EE | Olga Shumsky Matlin,
William McCune:
Encapsulation for Practical Simplification Procedures
CoRR cs.LO/0402010: (2004) |
| 2003 |
|---|
| 51 | EE | Olga Shumsky Matlin,
William McCune,
Ewing L. Lusk:
Methods to Model-Check Parallel Systems Software
CoRR cs.LO/0312012: (2003) |
| 50 | EE | William McCune:
Mace4 Reference Manual and Guide
CoRR cs.SC/0310055: (2003) |
| 49 | EE | William McCune:
OTTER 3.3 Reference Manual
CoRR cs.SC/0310056: (2003) |
| 2002 |
|---|
| 48 | EE | Olga Shumsky Matlin,
Ewing L. Lusk,
William McCune:
SPINning Parallel Systems Software.
SPIN 2002: 213-220 |
| 47 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 |
