Automated theorem proving applied to the theory of semigroups
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.
KeywordsInference Rule Inverse Semigroup Regular Semigroup Semigroup Theory Semi Group
Unable to display preview. Download preview PDF.
- Bundy, A. The Computer Modelling of Mathematical Reasoning, Academic Press, 1983.Google Scholar
- Howie, J. M., An Introduction to Semigroup Theory, Academic Press, 1976.Google Scholar
- Lallement, G., Some algorithmic problems in semigroup presentations, This volume, 1986.Google Scholar
- Lusk, E., McFadden, R., Using autoomated reasoning tools: A study of the Semigroup F2B2, Semigroup Forum (36), 1987, 75–88.Google Scholar
- Meakin, J., The free local semilattice on a set, to appear.Google Scholar
- Nambooripad, K. S. S., Structure of regular semigroups, Mem. Amer. Math. Soc. 224(1979).Google Scholar
- Wos, L., R. Overbeek, E. Lusk, J. Boyle, Automated Reasoning, Prentice Hall, 1984.Google Scholar
- 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