William McCune - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 47 from 47

2006

Otter/IvyMichael Beeson, William McCune. tphol 2006: 36-40 [doi]

Semantic Guidance for Saturation ProversWilliam McCune. AISC 2006: 18-24 [doi]

2002

SPINning Parallel Systems SoftwareOlga Shumsky Matlin, Ewing L. Lusk, William McCune. spin 2002: 213-220 [doi]

Short Single Axioms for Boolean AlgebraWilliam McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos. JAR, 29(1):1-16, 2002.

2000

System Description: IVYWilliam McCune, Olga Shumsky. cade 2000: 401-405

1998

Automatic Proofs and Counterexamples for Some Ortholattice IdentitiesWilliam McCune. ipl, 65(6):285-291, 1998. [doi]

1997

Otter - The CADE-13 Competition IncarnationsWilliam McCune, Larry Wos. JAR, 18(2):211-220, 1997.

Well-Behaved Search and the Robbins ProblemWilliam McCune. RTA 1997: 1-7

Solution of the Robbins ProblemWilliam McCune. JAR, 19(3):263-276, 1997.

Direct finite first-order model generation with negative constraint propagation heuristicOlga Shumsky, Ralph W. Wilkerson, William McCune, Fikret Erçal. SAC 1997: 25-29 [doi]

1996

Automated Deduction in Equational Logic and Cubic CurvesWilliam McCune, R. Padmanabhan. Volume 1095 of Lecture Notes in Computer Science, Springer, 1996.

1994

Distributed Theorem Proving by PeersMaria Paola Bonacina, William McCune. cade 1994: 841-845

SCOTT: Semantically Constrained Otter System DescriptionJohn K. Slaney, Ewing L. Lusk, William McCune. cade 1994: 764-768

1993

Uniform Strategies: The CADE-11 Theorem Proving ContestEwing L. Lusk, William McCune. JAR, 11(3):317-331, 1993.

Single Axioms for the Left Group and the Right Group CalculiWilliam McCune. ndjfl, 34(1):132-139, 1993.

Single Axioms for Groups and Abelian Groups with Various OperationsWilliam McCune. JAR, 10(1):1-13, 1993.

1992

1991

The Absence and the Presence of Fixed Point CombinatorsWilliam McCune, Larry Wos. TCS, 87(1):221-228, 1991.

Automated Theorem Proving and Logic ProgrammingLarry Wos, William McCune. jlp, 11(1&2):1-53, 1991.

1990

1989

Maintaining state constraints in relational databases: a proof theoretic basisWilliam McCune, Lawrence J. Henschen. JACM, 36(1):46-68, 1989. [doi]

Automated Reasoning about Elementary Point-Set TopologyCynthia A. Wick, William McCune. JAR, 5(2):239-255, 1989.

1988

Challenge Equality Problems in Lattice TheoryWilliam McCune. cade 1988: 704-709

Un-Skolemizing Clause SetsWilliam McCune. ipl, 29(5):257-263, 1988.

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving ProgramsLarry Wos, William McCune. cade 1988: 714-729

1987

A Case Study in Automated Theorem Proving: Finding Sages in Combinatory LogicWilliam McCune, Larry Wos. JAR, 3(1):91-107, 1987.

1986

1985

Experiments with Semantic ParamodulationWilliam McCune, Lawrence J. Henschen. JAR, 1(3):231-261, 1985.

1984

The Linked Inference Principle, II: The User s ViewpointLarry Wos, Robert Veroff, B. Smith, William McCune. cade 1984: 316-332

1983

Semantic Paramodula tion for Horn SetsWilliam McCune, Lawrence J. Henschen. IJCAI 1983: 902-908

1982

Compiling Constraint-Checking Programs from First-Order FormulasLawrence J. Henschen, William McCune, Shamim A. Naqvi. adbt 1982: 145-169

Logic Machine Architecture: Kernel FuntionsEwing L. Lusk, William McCune, Ross A. Overbeek. cade 1982: 70-84

Logic Machine Architecture: Inference MechanismsEwing L. Lusk, William McCune, Ross A. Overbeek. cade 1982: 85-108

Sign in or sign up to see more results.

runs on WebDSL