Automated theorem proving applied to the theory of semigroups

  • R. B. McFadden
Conference paper
Part of the Lecture Notes in Mathematics book series (LNM, volume 1320)


An automated reasoning program may be used in many different ways to assist with research in mathematics and related fields. The program used here for research in semigroup theory is ITP (Interactive Theorem Prover), designed at Argonne National Laboratory and at Northern Illinois University. It is a general purpose program, flexible in that it may call upon one inference rule or another, with choice dependent upon a given task in a given environment. Each step is available for scrutiny by the user; runs may be stopped at any time, and changes may be made as the user dictates.

ITP has been used to generate several types of semigroups, and to provide detailed analyses of Green's relations on these examples. It has been used to establish connections between R, L and D, and between these relations and regularity. All the proofs generated are readily accessible, and in some cases exhibit novel features. These results are preliminary to the planned project of equipping ITP with sufficient knowledge of semigroup theory to enable it to prove theorems in more depth. A third use has been to use the defining axioms for a local semilattice to generate some facts about free such objects. The results, while elementary, are encouraging.


Inference Rule Inverse Semigroup Regular Semigroup Semigroup Theory Semi Group 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Blyth, T. S. and R. B. McFadden, Naturally ordered regular semigroups with a greatest idempotent, Proc. Roy. Soc. Edinburgh, 91A,107–122,1981.MathSciNetCrossRefzbMATHGoogle Scholar
  2. [2]
    Bundy, A. The Computer Modelling of Mathematical Reasoning, Academic Press, 1983.Google Scholar
  3. [3]
    Howie, J. M., An Introduction to Semigroup Theory, Academic Press, 1976.Google Scholar
  4. [4]
    Lallement, G., Some algorithmic problems in semigroup presentations, This volume, 1986.Google Scholar
  5. [5]
    Lusk, E., McFadden, R., Using autoomated reasoning tools: A study of the Semigroup F2B2, Semigroup Forum (36), 1987, 75–88.Google Scholar
  6. [6]
    Meakin, J., The free local semilattice on a set, to appear.Google Scholar
  7. [7]
    Nambooripad, K. S. S., Structure of regular semigroups, Mem. Amer. Math. Soc. 224(1979).Google Scholar
  8. [8]
    Schein, B. M., Pseudo-semilattices and pseudo-lattices, Izv. Vyss, Ucebn, Zaved. Mat. 2(117)(1972), 81–94 (in Russian).MathSciNetGoogle Scholar
  9. [9]
    Wos, L., R. Overbeek, E. Lusk, J. Boyle, Automated Reasoning, Prentice Hall, 1984.Google Scholar
  10. [10]
    Winker, S. K., L. Wos, E. L. Lusk, Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I, Mathematics of Computation, 37(156), 533–545.Google Scholar

Copyright information

© Springer-Verlag 1988

Authors and Affiliations

  • R. B. McFadden

There are no affiliations available

Personalised recommendations