Cancallative Semigroups and Ore's Quotient Condition
From: Ranganathan Padmanabhan
To: William McCune
Cc: Ranganathan Padmanabhan
Date: Wed, 29 Mar 2006 16:01:03 -0600
Subject: Prover9 input for quotient condition, please
Hi Bill,
I am writing an account of what we proved in Albuquerque on CS-
related problems.
A well-known theorem in CS says that a cancellation semigroup
satisfying a non-trivial identity must satisfy the Ore's quotient
condition.
i.e. {CS, x*f*y = y*g*x} ==> Ore's quotient condition which is
a * a0 = b * b0.
c * a0 = d * b0.
a * c0 = b * d0.
implies c * c0 = d * d0
Some candidates of x*f*y = y*g*x for experimentation.
1. commutativity x*y = y*x. This proof must come very quickly
2. (x * y)^3 = x^3 * y^3.
3. (x * y)^3 = (y * x)^3.
In our Monograph, we have proved , using Otter, the same result with
x*y*z*y*x = y*x*z*x*y (the nilpotent class 2 case).
(see Theorem CS-13 on page 104).
Please try the above three examples and send me a Prover9 input file.
Thanks.
R. P.
Commutativity.
prover9 -f quot-comm.in > quot-comm.out ; ### ( quot-comm.out.xml )
Nilpotent Class 2.
prover9 -f quot-np2.in > quot-np2.out ; ### ( quot-np2.out.xml )
(xy)^3 = x^3 y^3.
prover9 -f quot-xy3a.in > quot-xy3a.out ; ### ( quot-xy3a.out.xml )
(xy)^3 = (yx)^3.
prover9 -f quot-xy3b.in > quot-xy3b.out ; ### ( quot-xy3b.out.xml )
The general case x * f(x,y) * y = y * g(x,y) * x.
prover9 -f quot-general.in > quot-general.out ; ### ( quot-general.out.xml )