Demo Data from EDBT 2026 / reviewers in the wild / expert
William McCune
dblp:m/WilliamMcCune · also William W. McCune
· DBLP profile ↗
36ranked-venue papers
20as first author
0since 2021 · last 2002
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Artificial intelligence and machine learning · 30 · 15 first-authorTheory of computation · 22 · 9 first-authorDatabases, data management, data science and information retrieval · 2 · 2 first-authorGraphics, computer vision, multimedia, augmented reality and games · 2 · 2 first-authorSoftware engineering, systems software and programming languages · 1Applied, interdisciplinary, general and emerging computing · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
2 papers |
Automated reasoning and model checking · 73% Logic in computer science · 27% | |
| Databases, data mining, and information retrieval
1 paper |
Database system architecture and tuning · 67% Database theory · 33% |
Topics — the 9 heaviest of 9, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking
automated theorem proving |
0.0 | 1 | 1990 | Skolem Functions and Equality in Automated Deduction · AAAI 1990 |
Automated reasoning and model checking
equational reasoning |
0.0 | 1 | 1990 | Skolem Functions and Equality in Automated Deduction · AAAI 1990 |
Logic in computer science › first-order logic
skolem functions |
0.0 | 1 | 1990 | Skolem Functions and Equality in Automated Deduction · AAAI 1990 |
Database theory
integrity constraints |
0.0 | 1 | 1989 | Maintaining state constraints in relational databases: a proof theoretic basis · J. ACM 1989 |
Database system architecture and tuning
integrity constraint maintenance |
0.0 | 1 | 1989 | Maintaining state constraints in relational databases: a proof theoretic basis · J. ACM 1989 |
Database system architecture and tuning
relational database system |
0.0 | 1 | 1989 | Maintaining state constraints in relational databases: a proof theoretic basis · J. ACM 1989 |
Automated reasoning and model checking
automated reasoning |
0.0 | 1 | 1983 | Semantic Paramodulation for Horn Sets · IJCAI 1983 |
Automated reasoning and model checking › equational reasoning
paramodulation |
0.0 | 1 | 1983 | Semantic Paramodulation for Horn Sets · IJCAI 1983 |
Knowledge, reasoning and agents › Knowledge representation and reasoning
logic-based reasoning |
0.0 | 1 | 1983 | Semantic Paramodulation for Horn Sets · IJCAI 1983 |
Methods — techniques the papers use, named apart from their topics
sufficient test · 0.0proof-theoretic method · 0.0complete test · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2002 | Short Single Axioms for Boolean Algebra
William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos |
J. Autom. Reason. | 1 |
| 2000 | System Description: IVY
William McCune, Olga Shumsky |
CADE | 1 |
| 1998 | Automatic Proofs and Counterexamples for Some Ortholattice Identities
William McCune |
Inf. Process. Lett. | 1 |
| 1997 | Well-Behaved Search and the Robbins Problem
William McCune |
RTA | 1 |
| 1997 | Solution of the Robbins Problem
William McCune |
J. Autom. Reason. | 1 |
| 1997 | Otter - The CADE-13 Competition Incarnations
William McCune, Larry Wos |
J. Autom. Reason. | 1 |
| 1994 | Distributed Theorem Proving by Peers
Maria Paola Bonacina, William McCune |
CADE | 2 |
| 1994 | SCOTT: Semantically Constrained Otter System Description
John K. Slaney, Ewing L. Lusk, William McCune |
CADE | 3 |
| 1993 | Uniform Strategies: The CADE-11 Theorem Proving Contest
Ewing L. Lusk, William McCune |
J. Autom. Reason. | 2 |
| 1993 | Single Axioms for Groups and Abelian Groups with Various Operations
William McCune |
J. Autom. Reason. | 1 |
| 1992 | ROO: A Parallel Theorem Prover
Ewing L. Lusk, William McCune, John K. Slaney |
CADE | 2 |
| 1992 | Experiments in Automated Deduction with Condensed Detachment
William McCune, Larry Wos |
CADE | 1 |
| 1992 | Application of Automated Deduction to the Search for Single Axioms for Exponent Groups
William McCune, Larry Wos |
LPAR | 1 |
| 1992 | Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi
William McCune |
J. Autom. Reason. | 1 |
| 1992 | Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval
William McCune |
J. Autom. Reason. | 1 |
| 1991 | The Absence and the Presence of Fixed Point Combinators
William McCune, Larry Wos |
Theor. Comput. Sci. | 1 |
| 1990 | Skolem Functions and Equality in Automated Deduction
William McCune |
AAAI | 1 |
| 1990 | Tutorial on High-Performance Automated Theorem Proving
Ewing L. Lusk, William McCune |
CADE | 2 |
| 1990 | OTTER 2.0
William McCune |
CADE | 1 |
| 1990 | Automated Reasoning Contributed to Mathematics and Logic
Larry Wos, Steven K. Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph M. Butler |
CADE | 3 |
| 1989 | Maintaining state constraints in relational databases: a proof theoretic basisabstractIf a relational database is required to satisfy a set of integrity constraints, then when the database is updated, one must ensure that it continues to satisfy the constraints. It is desirable not to have to evaluate each constraint after each update. A method is described that takes a constraint C and a class of updates, and either proves that an update in the class cannot violate C , or produces a formula C' (a complete test) that is satisfied before the update if and only if C would continue to be satisfied were the update to occur. C' is frequently much easier to evaluate than C . In addition, a formula D (a sufficient test) is sometimes produced such that if D is satisfied before the update, then C would continue to be satisfied were the update to occur. The method is proved correct. The method is substantially more general than other reported techniques for this problem. The method has been implemented, and a number of experiments with the implementation are presented. William McCune, Lawrence J. Henschen |
J. ACM | 1 |
| 1989 | Automated Reasoning about Elementary Point-Set Topology
Cynthia A. Wick, William McCune |
J. Autom. Reason. | 2 |
| 1988 | Challenge Equality Problems in Lattice Theory
William McCune |
CADE | 1 |
| 1988 | Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs
Larry Wos, William McCune |
CADE | 2 |
| 1988 | Un-Skolemizing Clause Sets
William McCune |
Inf. Process. Lett. | 1 |
| 1987 | A Case Study in Automated Theorem Proving: Finding Sages in Combinatory Logic
William McCune, Larry Wos |
J. Autom. Reason. | 1 |
| 1986 | Paths to High-Performance Automated Theorem Proving
Ralph M. Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
CADE | 3 |
| 1986 | ITP at Argonne National Laboratory
Ewing L. Lusk, William McCune, Ross A. Overbeek |
CADE | 2 |
| 1986 | Negative Paramodulation
Larry Wos, William McCune |
CADE | 2 |
| 1986 | Parallel Logic Programming for Numeric Applications
Ralph M. Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
ICLP | 3 |
| 1986 | Set Theory in First-Order Logic: Clauses for Gödel's Axioms
Robert S. Boyer, Ewing L. Lusk, William McCune, Ross A. Overbeek, Mark E. Stickel, Larry Wos |
J. Autom. Reason. | 3 |
| 1985 | Experiments with Semantic Paramodulation
William McCune, Lawrence J. Henschen |
J. Autom. Reason. | 1 |
| 1984 | The Linked Inference Principle, II: The User's Viewpoint
Larry Wos, Robert Veroff, Barry Smith 0002, William McCune |
CADE | 4 |
| 1983 | Semantic Paramodulation for Horn Sets
William McCune, Lawrence J. Henschen |
IJCAI | 1 |
| 1982 | Logic Machine Architecture: Kernel Funtions
Ewing L. Lusk, William McCune, Ross A. Overbeek |
CADE | 2 |
| 1982 | Logic Machine Architecture: Inference Mechanisms
Ewing L. Lusk, William McCune, Ross A. Overbeek |
CADE | 2 |