A Study in Automated Reasoning about Abstract Algebra:
Control Strategies for Supported Deductions

Nikhil Swamy, May 2000

This work was submitted to the Departments of Cognitive Science and Mathematics at Hampshire College in May, 2000 towards the fulfillment of degree requirements.

The first two chapters below are presented as a tutorial of sorts in the basic principles of first order logic and the techniques of deductive automated theorem proving. The third and fourth chapters constitute the main original work of this study and may be read independently by the adept. The final chapter contains my perspectives on the field, progress made thus far and possible future avenues of research.

Chapter 1: Brief introduction to first order logic

Chapter 2: Overview of some techniques in automated theorem proving

Chapter 3: New control strategies for supported proofs

Chapter 4: Searching for deep proofs and the use of term rewriting

Chapter 5: Perspectives and conclusion

Bibliography