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).
W. McCune and R. Padmanabhan, 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).
W. McCune and R. Padmanabhan, 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).
W. McCune and R. Padmanabhan, 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).
W. McCune and R. Padmanabhan, 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:
With MACE, a theorem in lattice theory was shown to fail for quasilattices:
W. McCune and R. Padmanabhan, Automated Deduction in Equational Logic and Cubic Curves, Springer-Verlag LNAI, to appear.
[email protected], [email protected]
W. McCune and R. Padmanabhan, Automated Deduction in Equational Logic and Cubic Curves, Springer-Verlag LNAI, to appear.
[email protected], [email protected]
W. McCune and R. Padmanabhan, 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
W. McCune and R. Padmanabhan, 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).
W. McCune and R. Padmanabhan, 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).
W. McCune and R. Padmanabhan, 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.
W. McCune and R. Padmanabhan, 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.