Pirog, Diane Carole
MetadataShow full item record
This paper is concerned with the general problem of theorem proving within a first order predicate logic. The topic was chosen as a result of simultaneous but separate interests in symbolic logic and Computer sciences. My involvement in proving theorems of a rather frustrating complexity led me to consider using a computer to perform the symbol and axiom manipulations associated with this type of proof. That this might have occurred to others did not occur to me in my first burst of enthusiasm. After studying an available program that proved theorems of a sentential calculus by means of truth values I searched in the journals and computer literature for leads to methods of symbol manipulation and found a reference to just such a program as I had hoped to construct: Newell, Shaw and Simonis Logic Theorist. To try to duplicate the work of more experienced minds working with more extensive equipment seemed contrary to the purpose of a Senior Project, but I was unwilling to discard either the topic or my preliminary research completely. Rather, my interest was increased by curiosity to see how earlier programmers had approached the problem and what had been achieved, and by a desire to find out what could be accomplished on the computer with this type of problem (for which it was proved by Church that there is no automatic test of validity).