24 Matching Results

Search Results

Advanced search parameters have been applied.

Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs

Description: In this paper, we offer a set of problems for evaluating the power of automated theorem-proving programs and the potential of new ideas. Since the problems published in the proceedings of the first CADE conference proved to be so useful, and since researchers are now far more disposed to implementing and testing their ideas, a new set of problems to complement those that have been widely studied is in order. In general, the new problems provide a far greater challenge for an automated theorem-proving program than those in the first set do. Indeed, to our knowledge, five of the six problems we propose for study have never been proved with a theorem-proving program. For each problem, we give a set of statements that can easily be translated into a standard set of clauses. We also state each problem in its mathematical and logical form. In many cases, we also provide a proof of the theorem from which a problem is taken so that one can measure a program's progress in its attempt to solve the problem. Two of the theorems we discuss are of especial interest in that they answer questions that had been open concerning the constructibility of two types of combinator. We also include a brief description of a new strategy for restricting the application of paramodulation. All of the problems we propose for study emphasize the role of equality. This paper is tutorial in nature.
Date: January 1, 1988
Creator: Wos, L. & McCune, W.
Partner: UNT Libraries Government Documents Department

Searching for fixed point combinators by using automated theorem proving: A preliminary report

Description: In this report, we establish that the use of an automated theorem- proving program to study deep questions from mathematics and logic is indeed an excellent move. Among such problems, we focus mainly on that concerning the construction of fixed point combinators---a problem considered by logicians to be significant and difficult to solve, and often computationally intensive and arduous. To be a fixed point combinator, THETA must satisfy the equation THETAx = x(THETAx) for all combinators x. The specific questions on which we focus most heavily ask, for each chosen set of combinators, whether a fixed point combinator can be constructed from the members of that set. For answering questions of this type, we present a new, sound, and efficient method, called the kernel method, which can be applied quite easily by hand and very easily by an automated theorem-proving program. For the application of the kernel method by a theorem-proving program, we illustrate the vital role that is played by both paramodulation and demodulation---two of the powerful features frequently offered by an automated theorem-proving program for treating equality as if it is ''understood.'' We also state a conjecture that, if proved, establishes the completeness of the kernel method. From what we can ascertain, this method---which relies on the introduced concepts of kernel and superkernel---offers the first systematic approach for searching for fixed point combinators. We successfully apply the new kernel method to various sets of combinators and, for the set consisting of the combinators B and W, construct an infinite set of fixed point combinators such that no two of the combinators are equal even in the presence of extensionality---a law that asserts that two combinators are equal if they behave the same. 18 refs.
Date: September 1, 1988
Creator: Wos, L. & McCune, W.
Partner: UNT Libraries Government Documents Department

A case study in automated theorem proving: A difficult problem about commutators

Description: This paper shows how the automated deduction system OTTER. was used to prove the group theory theorem {chi}{sup 3} = e {implies} [[[y, z], u], v] = e, where e is the identity, and [XI Y] is the commutator {chi}{prime}y{prime}{chi}y. This is a difficult problem for automated provers, and several lengthy searches were run before a proof was found. Problem formulation and search strategy played a key role in the success. I believe that ours is the first automated proof of the theorem.
Date: February 1, 1995
Creator: McCune, W.
Partner: UNT Libraries Government Documents Department

Single axioms for Boolean algebra.

Description: Explicit single axioms are presented for Boolean algebra in terms of (1) the Sheffer stroke; (2) disjunction and negation; (3) disjunction, conjunction, and negation; and (4) disjunction, conjunction, negation, 0, and 1. It was previously known that single axioms exist for these systems, but the procedures to generate them are exponential, producing huge equations. Automated deduction techniques were applied to find axioms of lengths 105, 131, 111, and 127, respectively, each with six variables.
Date: June 30, 2000
Creator: McCune, W.
Partner: UNT Libraries Government Documents Department

OTTER 3.3 reference manual.

Description: OTTER is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy. OTTER is coded in ANSI C, is free, and is portable to many different kinds of computer.
Date: October 27, 2003
Creator: McCune, W.
Partner: UNT Libraries Government Documents Department

Mace4 reference manual and guide.

Description: Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than did our previous model-searching program Mace2.
Date: October 27, 2003
Creator: McCune, W.
Partner: UNT Libraries Government Documents Department

MACE 2.0 reference manual and guide.

Description: MACE is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. MACE is a useful complement to the theorem prover Otter, with Otter searching for proofs and MACE looking for countermodels.
Date: June 8, 2001
Creator: McCune, W.
Partner: UNT Libraries Government Documents Department

A Short Sheffer axiom for Boolean algebra.

Description: A short Sheffer stroke identity is shown to be a single axiom for Boolean algebra. The axiom has length 15 and 3 variables. The proof shows that it is equivalent to Sheffer's original 3-basis for the theory. Automated deduction techniques were used to find the proof. The shortest single axiom previously known to us has length 105 and 6 variables.
Date: June 30, 2000
Creator: Veroff, R. & McCune, W.
Partner: UNT Libraries Government Documents Department

System description: IVY

Description: IVY is a verified theorem prover for first-order logic with equality. It is coded in ACL2, and it makes calls to the theorem prover Otter to search for proofs and to the program MACE to search for countermodels. Verifications of Otter and MACE are not practical because they are coded in C. Instead, Otter and MACE give detailed proofs and models that are checked by verified ACL2 programs. In addition, the initial conversion to clause form is done by verified ACL2 code. The verification is done with respect to finite interpretations.
Date: February 4, 2000
Creator: McCune, W. & Shumsky, O.
Partner: UNT Libraries Government Documents Department

Application of automated deduction to the search for single axioms for exponent groups

Description: 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 couterexamples. We also touch on relations between logic programming and automated reasoning.
Date: February 11, 1992
Creator: McCune, W. & Wos, L.
Partner: UNT Libraries Government Documents Department

FormEd: An X Window System application for managing first-order formulas

Description: FormEd is a window-based program for constructing, displaying, and managing first-order logic formulas. The main motivation for constructing FormEd was the desire to have formulas displayed in a readable, two-dimensional format. Users of FormEd can make two kinds of transformation on formulas: logic transformations, such as negation normal form translation, which preserve the meaning of a formula, and edit transformations, which can be used to make arbitrary changes, such as adding a hypothesis to a subformula. FormEd was written by using the X Window System, Version 11, and code from the theorem prover OTTER. 4 refs.
Date: November 1, 1990
Creator: Henry, T.L. & McCune, W.W.
Partner: UNT Libraries Government Documents Department

An entry in the 1992 Overbeek theorem-proving contest

Description: The Conference on Automated Deduction (CADE) has been for nearly twenty years a meeting where both theoreticians and system implementors present their work. Feeling perhaps that the conference was becoming dominated by the theoreticians, Ross Overbeek proposed at CADE-10 in 1990 a contest to stimulate work on the implementation and use of theorem-proving systems. The challenge was to prove a set of theorems, and do so with a uniform approach. That is, it was not allowed to set parameters in the system to specialize it for individual problems. There were actually two separate contests, one represented by a set of seven problems designed to test basic inference components, and the other represented by a set of ten problems designed to test equality-based systems. This paper describes our experiences in preparing to enter the contest with OTTER and Roo, two systems developed at Argonne National Laboratory. Roo is a parallel version of OTTER, but has such different behavior in some cases that we treat them as separate entries. We entered each of them in both contests. Some of the problems are difficult ones; and although many of the problems had been done before with OTTER, in each case we had set OTTER'S many input parameters in a way customized to the problem at hand, and chosen a set of support that appeared to us to be most natural. It was a challenge to come up with a uniform set of parameter settings and a information algorithm for picking the set of support that would allow OTTER to prove each of the theorems.
Date: November 1, 1992
Creator: Lusk, E.L. & McCune, W.W.
Partner: UNT Libraries Government Documents Department

Roo: A parallel theorem prover

Description: We describe a parallel theorem prover based on the Argonne theorem-proving system OTTER. The parallel system, called Roo, runs on shared-memory multiprocessors such as the Sequent Symmetry. We explain the parallel algorithm used and give performance results that demonstrate near-linear speedups on large problems.
Date: November 1, 1991
Creator: Lusk, E.L.; McCune, W.W. & Slaney, J.K.
Partner: UNT Libraries Government Documents Department

SPINning parallel systems software.

Description: We describe our experiences in using Spin to verify parts of the Multi Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of processes connected by Unix network sockets. MPD is dynamic processes and connections among them are created and destroyed as MPD is initialized, runs user processes, recovers from faults, and terminates. This dynamic nature is easily expressible in the Spin/Promela framework but poses performance and scalability challenges. We present here the results of expressing some of the parallel algorithms of MPD and executing both simulation and verification runs with Spin.
Date: March 15, 2002
Creator: Matlin, O.S.; Lusk, E. & McCune, W.
Partner: UNT Libraries Government Documents Department

Single identities for lattice theory and for weakly associative lattices

Description: We present a single identity for the variety of all lattices that is much simpler than those previously known to us. We also show that the variety of weakly associative lattices is one-based, and we present a generalized one-based theorem for subvarieties of weakly associative lattices that can be defined with absorption laws. The automated theorem-proving program OTTER was used in substantial way to obtain the results.
Date: March 13, 1995
Creator: McCune, W. & Padmanabhan, R.
Partner: UNT Libraries Government Documents Department

An equational characterization of the conic construction of cubic curves

Description: An n-ary Steiner law f(x{sub 1},x{sub 2},{hor_ellipsis},x{sub n}) on a projective curve {Gamma} over an algebraically closed field k is a totally symmetric n-ary morphism f from {Gamma}{sup n} to {Gamma} satisfying the universal identity f(x{sub 1},x{sub 2},{hor_ellipsis},x{sub n-1}, f(x{sub 1},x{sub 2},{hor_ellipsis},x{sub n})) = x{sub n}. An element e in {Gamma} is called an idempotent for f if f(e,e,{hor_ellipsis},e) = e. The binary morphism x * y of the classical chord-tangent construction on a nonsingular cubic curve is an example of a binary Steiner law on the curve, and the idempotents of * are precisely the inflection points of the curve. In this paper, the authors prove that if f and g are two 5-ary Steiner laws on an elliptic curve {Gamma} sharing a common idempotent, then f = g. They use a new rule of inference rule =(gL){implies}, extracted from a powerful local-to-global principal in algebraic geometry. This rule is implemented in the theorem-proving program OTTER. Then they use OTTER to automatically prove the uniqueness of the 5-ary Steiner law on an elliptic curve. Very much like the binary case, this theorem provides an algebraic characterization of a geometric construction process involving conics and cubics. The well-known theorem of the uniqueness of the group law on such a curve is shown to be a consequence of this result.
Date: May 17, 1995
Creator: McCune, W. & Padmanabhan, R.
Partner: UNT Libraries Government Documents Department

Short equational bases for ortholattices : proofs and countermodels.

Description: This document contains proofs and countermodels in support of the paper ''Short Equational Bases for Ortholattices'', by the same set of authors. In that paper, short single axioms for ortholattices, orthomodular lattices, and modular ortholattices are presented, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. Other equational bases in terms of the Sheffer stroke and in terms of join, meet, and complement are presented. Computers were used extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.
Date: January 9, 2004
Creator: McCune, W.; Padmanabhan, R.; Rose, M. A. & Veroff, R.
Partner: UNT Libraries Government Documents Department

Methods to model-check parallel systems software.

Description: We report on an effort to develop methodologies for formal verification of parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of communicating processes. While the individual components of the collection execute simple algorithms, their interaction leads to unexpected errors that are difficult to uncover by conventional means. Two verification approaches are discussed here: the standard model checking approach using the software model checker SPIN and the nonstandard use of a general-purpose first-order resolution-style theorem prover OTTER to conduct the traditional state space exploration. We compare modeling methodology and analyze performance and scalability of the two methods with respect to verification of MPD.
Date: December 15, 2003
Creator: Matlin, O. S.; McCune, W. & Lusk, E.
Partner: UNT Libraries Government Documents Department

An entry in the 1992 Overbeek theorem-proving contest

Description: The Conference on Automated Deduction (CADE) has been for nearly twenty years a meeting where both theoreticians and system implementors present their work. Feeling perhaps that the conference was becoming dominated by the theoreticians, Ross Overbeek proposed at CADE-10 in 1990 a contest to stimulate work on the implementation and use of theorem-proving systems. The challenge was to prove a set of theorems, and do so with a uniform approach. That is, it was not allowed to set parameters in the system to specialize it for individual problems. There were actually two separate contests, one represented by a set of seven problems designed to test basic inference components, and the other represented by a set of ten problems designed to test equality-based systems. This paper describes our experiences in preparing to enter the contest with OTTER and Roo, two systems developed at Argonne National Laboratory. Roo is a parallel version of OTTER, but has such different behavior in some cases that we treat them as separate entries. We entered each of them in both contests. Some of the problems are difficult ones; and although many of the problems had been done before with OTTER, in each case we had set OTTER`S many input parameters in a way customized to the problem at hand, and chosen a set of support that appeared to us to be most natural. It was a challenge to come up with a uniform set of parameter settings and a information algorithm for picking the set of support that would allow OTTER to prove each of the theorems.
Date: November 1, 1992
Creator: Lusk, E. L. & McCune, W. W.
Partner: UNT Libraries Government Documents Department

Roo: A parallel theorem prover

Description: We describe a parallel theorem prover based on the Argonne theorem-proving system OTTER. The parallel system, called Roo, runs on shared-memory multiprocessors such as the Sequent Symmetry. We explain the parallel algorithm used and give performance results that demonstrate near-linear speedups on large problems.
Date: November 1, 1991
Creator: Lusk, E. L.; McCune, W. W. & Slaney, J. K.
Partner: UNT Libraries Government Documents Department