Author name cluster

William McCune

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

LPAR Conference 1992 Conference Paper

Application of Automated Deduction to the Search for Single Axioms for Exponent Groups

William McCune
Larry Wos

Abstract We present new results in axiomatic group theory obtained by using automated deduction programs. The results include single axioms, some with the identity and others without, for groups of exponents 3, 4, 5, and 7, and a general form for single axioms for groups of odd exponent. The results were obtained by using the programs in three separate ways: as a symbolic calculator, to search for proofs, and to search for counterexamples. We also touch on relations between logic programming and automated reasoning.

Details

TCS Journal 1991 Journal Article

The absence and the presence of fixed point combinators

William McCune
Larry Wos

In this article we give some classes of fragments of weak combinatory logic and show that they fail to admit various fixed point properties. We also present the results of a new technique, the kernel strategy, for using an automated theorem-proving program to search for fixed point combinators within a given fragment. A key aspect of the work is that experimentation with the kernel strategy led indirectly to proofs of theorems concerning the absence of the fixed point properties.

Details DOI

AAAI Conference 1990 Conference Paper

Skolem Functions and Equality in Automated Deduction

William McCune

We present a strategy for restricting the application of the inference rule paramodulation. The strategy applies to problems in first-order logic with equality and is designed to prevent paramodulation into subterms of Skolem expressions. A weak completeness result is presented (the functional reflexive axioms are assumed). Experimental results on problems in set theory, combinatory logic, Tarski geometry, and algebra show that the strategy can be useful when searching for refutations and when applying Knuth-Bendix completion. The emphasis of the paper is on the effectiveness of the strategy rather than on its completeness.

PDF Details