- The NIUTP/AURA series of the 1970s and early 1980s
- LMA/ITP of the 1980s
- Otter, our current prover
- EQP, an experimental AC prover for equational logic
- MACE, a model searcher

- Algebraic Geometry
- Cancellative Semigroups
- Lattice Theory
- Quasilattice Theory
- Uniqueness of Operations in Lattice-like Algebras
- Self-dual Bases for Boolean Algebra
- Self-dual 2-Basis for Group Theory
- Self-dual Bases for Group Varieties
- Quasigroup Theory
- Quasigroup Design Problems
- Single Axioms for Ternary Boolean Algebra
- Single Axioms for Groups
- Simple Bases for Moufang Loops
- Single Axioms for Inverse Loops and Subvarieties
- Left Group and Right Group Calculi
- Fixed Point Combinators
- Semigroup Structure (F3B2)
- Illative Combinatory Logic (Jech)
- Robbins Algebra and Boolean Algebra
- Equivalential Calculus Single Axioms
- Semigroups, Antiautomorphisms, and Involutions
- Independence of Ternary Boolean Algebra Axioms
- Two-valued Sentential Calculus
- Many-valued Sentential Calculus
- Short Proofs in Various Logic Calculi
- Pure Proofs in Equivalential Calculus

R. Padmanabhan and W. McCune,
``Automated Reasoning about Cubic Curves'',
*Computers and Mathematics with Applications* 29(2), 17-26 (1995).

[email protected], [email protected]

In fact, Otter showed that associativity can be replaced
with the (weaker) pair of equations
{*x(yx)=(xy)x, x(xy)=(xx)y*}, or with any of several weaker
forms of associativity such as *x(y(zu)) = ((xy)z)u*.

W. McCune and R. Padmanabhan,
*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

*f(e,e,e,e,e)=e, f(f(x,y,e,e,e),y,e,e,e) = x, f* is symmetric,

*g(e,e,e,e,e)=e, g(g(x,y,e,e,e),y,e,e,e) = x, g* is symmetric

(symmetry means that the arguments can be permuted in any way).
Then *S* =(gL)=> *f(x,y,z,u,v) = g(x,y,z,u,v)*.

A corollary of this theorem is the following. Consider the conic determined by 5 points on a cubic curve. Then the sixth point of intersection can be obtained by a simple ruler construction.

R. Padmanabhan and W. McCune, ``An Equational Characterization of the Conic Construction on Cubic Curves'', preprint MCS-P517-0595, Argonne National Laboratory, 1995.

W. McCune and R. Padmanabhan,
*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

{*xyzyx=yxzxy*} => {*xyyx=yxxy*}

by letting *z* be the identity. The statement holds also for
cancellative semigroups, but the proof is more difficult.

In working on the conjecture and searching for a counterexample, we have used Otter to generalize many theorems in group theory to cancellative semigroups, for example,

{*x y^3 = y^3 x*} => {*(xy)^9 = x^9 y^9*}, and

{*xyyyxy = yyyyxx*} => {*yxyyyx = xxyyyy*}.

W. McCune and R. Padmanabhan,
*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

L1. *(y join (x meet (y meet z))) = y*

L2. *(y meet (x join (y join z))) = y*

L3. *(((x meet y) join (y meet z)) join y) = y*

L4. *(((x join y) meet (y join z)) meet y) = y*

By examining many candidate sets with Otter, we found an alternative axiomatization in which the pair L1 and L4 are replaced with

L4'. *(((y join x) meet (y join z)) meet y) = y*.

W. McCune and R. Padmanabhan, ``Single Identities for Lattice Theory and for Weakly Associative Lattices'', Algebra Universalis, to appear ( preprint MCS-P493-0395).

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

*p(p(x,y,y),p(x,p(y,z,F(y)),G(y)),u)=y*,

where *F(y)* and *G(y)* are to be replaced with absorption
identities.

W. McCune and R. Padmanabhan, ``Single Identities for Lattice Theory and for Weakly Associative Lattices'', Algebra Universalis, to appear ( preprint MCS-P493-0395).

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

W. McCune and R. Padmanabhan, ``Single Identities for Lattice Theory and for Weakly Associative Lattices'', Algebra Universalis, to appear ( preprint MCS-P493-0395).

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

With Otter, several results in lattice theory were proved for quasilattices:

- A distributive law implies its dual.
- Bowden's inequality,
*x join (y meet z) >= (x join y) meet z*, implies distributivity. - Self-dual forms of distributivity and modularity.

With MACE, a theorem in lattice theory was shown to fail for quasilattices:

- A quasilattice (but not a lattice) can have two distinct meet (dually, join) operations.

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

- (MACE) a quasilattice
*can*have two meets; - (Otter) a weakly associative lattice
*cannot*have two meets; - (MACE) a ternary near lattice
*can*have two meets.

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

Here, a set *S* of equalities is self-dual if for each equality
*E* in *S*, its mirror image *d(E)* is also in *S*.
Size 2 was the only open case. A large set of candidate pairs was
enumerated, and Otter answered *yes* by proving that the following pair
axiomatizes groups.

*((x y) z) (y z)' = x*

*(z y)' (z (y x)) = x*

The analogous question for Abelian groups was also open, and Otter answered that question positively as well, with the following pair.

*(z (x y)) (y z)' = x*

*(z y)' ((y x) z) = x*

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

Theorem. Let *E* be an equational subvariety of group theory.
then there exists an independent self-dual *n*-basis for *E*,
for *n*>1.

We conjectured various schemas, Otter proved cases *n*=2,3,4,
and the rest was by hand (with induction).

W. McCune and R. Padmanabhan,
*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.
(cases 2,3,4).

The full proof will be published separately.

[email protected], [email protected]

We have several new results on consequences of (and relationships between) the Thomsen closure condition (TC), the Reidemeister closure condition (RC) and Padmanabhan's overlay condition. [[Get most significant examples from RP.]]

These proofs were obtained by Otter (without our guidance).

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

Several open questions on the existence of finite quasigroups were answered with the model searcher MACE. The questions were about Mendelsohn triple systems and self-orthogonal Latin squares. See the MACE quasigroup page for details.

W. McCune, ``A Davis-Putnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems'', Tech. Memo. ANL/MCS-TM-194, Argonne National Laboratory, 1994.

R. Padmanabhan and W. McCune,
``Single Identities for Ternary Boolean Algebras'',
*Computers and Mathematics with Applications* 29(2), 13-16 (1995).

[email protected], [email protected]

Product and inverse: *(x(y(((zz')(uy)')x))') = u*

Division and identity: *((e / (x / (y / (((x / x) / x) / z)))) / z) = y*

Division and inverse: *((x / x) / (y / ((z / (u / y)) / u'))) = z*

Double inversion and identity: *((x # (((x # y) # z) # (y # e))) # (e # e)) = z*

Double inversion and inverse: *(x' # ((x # (y # z))' # (u # (y # u)))') = z*

Ken Kunen showed later that no axiom in terms of product and inverse is shorter than the one given above.

W. McCune,
``Single Axioms for Groups and Abelian Groups with Various Operations'',
*J. Automated Reasoning* 10(1), 1-13 (1993).

Product and inverse: *(((xy)z)(xz)')=y*

Division and identity: *((e / (((x / y) / z) / x)) / z) = y*

Division and inverse: *((x / (y / (x / z))') / z) = y*

Double inversion and identity: *((x # ((z # (x # y)) # (e # y))) # (e # e)) = z*

Double inversion and inverse: *(x # (((x # y) # z')' # y)') = z*

W. McCune,
``Single Axioms for Groups and Abelian Groups with Various Operations'',
*J. Automated Reasoning* 10(1), 1-13 (1993).

A group of exponent *n* satisfies *x^n=e* (the identity element);
such theories can be axiomatized with product alone.
With Otter, we found
single axioms for *n=3,5,7*, then noticed a pattern in the
form of the axioms and in the proofs, then proved (by hand) that
the pattern works for all odd *n*. We also found
a pattern, in terms of product and identity, for odd exponents.
Examples (terms are right associated):

*xx(xxxyzzzz)z=y* [exponent 5]

*xxx(xxxxyzzzzzz)z=y* [exponent 7]

*xx(xx(xy)z)ezzzz=y* [exponent 5, with e]

*xxx(xxx(xy)z)ezzzzzz=y* [exponent 7, with e]

We found that even exponents are much more difficult.

W. McCune and L. Wos,
``Application of Automated Deduction to the Search for Single Axioms
for Exponent Groups'',
*Proc. of LPAR*, Springer-Verlag LNCS #624, 131-136 (1992).

[email protected], [email protected]

The goal was to find short single axioms for several types of permutative group. (By a result of B. H. Neumann, single axioms for the varieties in question can be constructed, but they are large.) By running Otter proof searches with large numbers of candidates, single axioms were discovered for several varieties:

*xxy=yxx* groups: *((xy')'((zz)(xu)))(u(zz))'=y*

*xxyy=yyxx* groups: *(((x(x(yy)))z)'u)(((y(y(xx)))(zv))'u)'=v*

From the second of these, Ken Kunen later derived a schema, much simpler than Neumann's, for building single axioms for varieties of groups.

Not published.

ABSTRACT.
We study equations of the form *(alpha = x)* which are single axioms for group
theory. Earlier examples of such were found by Neumann and McCune.
We prove some lower bounds on the complexity of these *alpha*, showing
that McCune's examples are the shortest possible. We also show
that no such *alpha* can have only two distinct variables.
We do produce an *alpha* with only three distinct variables, refuting
a conjecture of Neumann. Automated reasoning techniques are used
both positively (searching for and verifying single axioms)
and negatively (proving that various candidate *(alpha = x)* hold in some
non-group and are hence not single axioms).

ABSTRACT.
We study equations of the form *(alpha = x)* which are single axioms for
groups of exponent 4, where *alpha* is a term in product only.
Every such *alpha* must have at least nine variable occurrences,
and there are exactly three such *alpha* of this size,
up to variable renaming and mirroring.
These terms were found by an exhaustive search through all
terms of this form. Automated techniques were
used in two ways: to eliminate many *alpha* by verifying
that *(alpha = x)* is true in some non-group, and to verify
that the group axioms do indeed follow from the successful *(alpha = x)*.
We also present an improvement on Neumann's scheme for single
axioms for varieties of groups.

ABSTRACT. With the aid of automated reasoning techniques, we show that all previously known short single axioms for odd exponent groups are special cases of one general schema. We also demonstrate how to convert the proofs generated by an automated reasoning system into proofs understandable by a human.

[email protected], [email protected]

*1x = x*

*x'x = 1*

*((xy)z)y = x(y(zy))* % Moufang-2

It was also found that Moufang-2 can be replaced with Moufang-3 (Otter), but not with Moufang-1 (MACE).

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

*x((((xy')y)'z)(u'u)) = z*. % 2158

This was then generalized to a schema for equational subvarieties of inverse loops:

*x((((xy')y)'z)((alpha u)'(beta u))) = z*.

The terms *alpha* and *beta* specify the subvariety of interest.
This gives us single axioms for Moufang loops, groups, Abelian groups, etc.

*Automated Deduction in Equational Logic and Cubic Curves*, Springer-Verlag LNAI, to appear.

[email protected], [email protected]

Group theory can be axiomatized without equality, using the division operation, with instantiation and the detachment rule:

If *x/y* is 1 and *y* is 1, then *x* is 1.

This is the left group calculus (for the right calculus, change *x/y*
to *y/x*). No single axioms were previously known.
Large sets (tens of thousands) of candidates were constructed, and
an Otter search was run on each candidate, trying to show it to be a single
axiom. Single axioms for each of the calculi were discovered, for example,

*(((x/y)/z)/((u/v)/(((w/v)/(w/u))/s)))/(z/((y/x)/s))* [left],

*x/(x/((y/z)/((y/u)/(z/u))))* [right].

W. McCune,
``Single Axioms for the Left Group and Right Group Calculi'',
*Notre Dame J. Formal Logic* 34(1), 132-139 (1993).

W. McCune,
``Automated Discovery of New Axiomatizations of the Left Group and
Right Group Calculi'',
*J. Automated Reasoning* 9(1), 1-24 (1992).

Weak -- all *x* exists *y*, *xy=y*
[every combinator has a fixed point].

Strong -- exists *Q* all *x*, *x(Qx) = Qx*
[*Q* is a fixed-point-finder].

Many fragments were shown (directly, with Otter) to satisfy the weak property or both of the properties, and many fragments and classes of fragments were shown (automatically with MACE, or by hand, with insight from failed Otter searches) to fail the strong property or both of the properties.

A specialized technique, the *kernel strategy*, was developed to
search for fixed point combinators; many new results were obtained
by using the strategy with Otter. (An important question that remains
open is whether the fragment {*M,B*} satisfies the strong property.)

W. McCune and L. Wos,
``The Absence and the Presence of Fixed Point Combinators'',
*Theoretical Computer Science* 87, 221-228 (1991).

L. Wos
``The Kernel Strategy and Its Use for the Study of Combinatory Logic'',
*J. Automated Reasoning* 10(3), 287-343 (1993).

{mccune,wos}@mcs.anl.gov

[[Get abstract from Lusk.]]

E. Lusk and R. McFadden.

[email protected], [email protected]

T. Jech,
``OTTER Experiments in a System of Combinatory Logic'',
*J. Automated Reasoning* 14(3), 413--426 (1995).

ABSTRACT. This paper describes some experiments involving the automated theorem-proving program Otter in the system TRC of illative combinatory logic. We show how Otter can be steered to find a contradiction in an inconsistent variant of TRC, and present some experimentally discovered identities in TRC.

The Robbins problem has been solved. See the
*Robbins Algebra Page*.

{swinker,wos,mccune}@mcs.anl.gov

Exactly seven length-11 theorems of the equivalential calculus (EC) were unclassified in regard to their being single axioms for EC. Two were shown to be single axioms by using the theorem prover AURA. Four were shown to be too weak to be single axioms; in these cases, the proofs were produced mostly by hand using insight gained from failed attempts at automated proofs.

L. Wos, S. Winker, R. Veroff, B. Smith, and L. Henschen,
``Questions Concerning Possible Shortest Single Axioms in Equivalential
Calculus: An Application of Automated Theorem Proving to Infinite Domains'',
*Notre Dame J. Formal Logic* 24(2), 205-223 (1983).

{wos,swinker}@mcs.anl.gov, [email protected]

*Does there exist a finite semigroup admitting a nontrivial antiautomorphism
but no nontrivial involution?*

The answer was shown to be *yes* by using one of the NIUTP/AURA theorem
provers in nonstandard ways to search for models. Four models of
order 7 were found, and it was shown that there are no others of size
less than or equal to 7.

S. Winker, L. Wos, and E. Lusk,
``Semigroups, Antiautomorphisms, and Involutions: A Computer Solution
to an Open Problem, I'',
*Math. of Comp.* 37, 533-545 (1981).

{swinker,wos,lusk}@mcs.anl.gov

(1) * f(f(v,w,x),y,f(v,w,z)) = f(v,w,f(x,y,z))*

(2) * f(y,x,x) = x*

(3) * f(x,y,g(y)) = x*

(4) * f(x,x,y) = x*

(5) * f(g(y),y,x) = x*

It was previously known that (4) and (5) together are dependent on (1), (2), and (3). Using one of the NIUTP/AURA theorem provers in a nonstandard way to search for models, it was shown that each of (1), (2), and (3) is independent of the remaining four axioms.

S. Winker, ``Generation and Verification of Finite Models and Counterexamples
Using an Automated Theorem Prover Answering Two Open Questions'',
*J. ACM* 29, 273-284 (1982).

*i(i(x,y),i(i(y,z),i(x,z)))*

*i(i(n(x),x),x)*

*i(x,i(n(x),y))*

with the inference rule condensed detachment. A new axiom system was found with OTTER, consisting of theses 19, 37, and 60.

Other axiom systems had already been known, due to Church, Frege, Hilbert, and (an alternate of) Lukasiewicz. With a methodology relying on a variety of strategies, shorter proofs of the various axiom systems were found, using as hypothesis the three listed Lukasiewicz axioms.

L. Wos,
``Automated Reasoning and Bledsoe's Dream for the Field'',
*Automated Reasoning: Essays in Honor of Woody Bledsoe*,
ed. R. S. Boyer, Kluwer Academic Publishers: Dordrecht, 1991.

*i(x,i(y,x))*

*i(i(x,y),i(i(y,z),i(x,z)))*

*i(i(i(x,y),y),i(i(y,x),x))*

*i(i(n(x),n(y)),i(y,x)*

with the inference rule condensed detachment. The following formula, once thought by Lukasiewicz to be required as an axiom, is in fact dependent.

*i(i(i(x,y),i(y,x)),i(y,x))*

Otter was used to find the first unguided proof of this fact with
condensed detachment as the inference rule. Further, Otter eventually
was used to find a 34-step proof of this fact, a proof far shorter
than previously known, and a proof in which no terms of the form
*n(n(t))* are present, also conjectured to be unobtainable.

L. Wos,
*The Automation of Reasoning: An Experimenter's Notebook with Otter Tutorial*,
Academic Press, to appear.

L. Wos,
``The Power of Combining Reasonance with Heat'',
*J. Automated Reasoning*, to appear
(
preprint P522.ps.Z).

L. Wos,
``Searching for Circles of Pure Proofs'',
*J. Automated Reasoning* 15, pp. 279-315, 1995
(
preprint P479.ps.Z).

*
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.
*