🚀 go-pugleaf

In article <1g282rINN5ja@eagle.dfki.uni-sb.de> treinen@dfki.uni-sb.de (Ralf Treinen) writes:

   In article <19921208.075322039663.NETNEWS@ALIJKU11>, groda@risc.uni-linz.ac.at (Giovanna Roda) writes:
   |> Suppose we are given an axiomatization for the theory of groups consisting
   |> of the following three axioms:
   |> (x*y)*z=x*(y*z)
   |> Vy x=y*z
   |> Vz x=y*z
   |> (where V is the existential quantifier).
   |> Is this theory decidable?

   No. This has been proven in

   @InCollection{Tar:groups53,
   author	= "Alfred Tarski",
   title	= "Undecidability in the Elementary Theory of Groups",
   pages	= "75--87",
   crossref= "TMR:Undecidable53"
   }

No I am slightly confused. Am I wrong remembering that the followoing
presentation of groups

	(x*y)*z=x*(y*z)
	x*e = x
	e*x = x
	i(x)*x = e
	x*i(x) = e

could be completed using the Knuth-Bendix algorithm & therefore is
decidable. How does this relate to the above mentioned result?

--

 Thorsten Altenkirch         	And there's a hand, my trusty fiere,
 Laboratory for Foundations  	   And gie's a hand o' thine,
 of Computer Science 	      	And we'll tak a right guid-willie waught
 University of Edinburgh     	   For auld lang syne!