Algorithms
Loading...
Authors
Pirog, Diane Carole
Issue Date
1966
Type
Thesis
Language
en_US
Keywords
Alternative Title
Abstract
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).
Description
iii, 122 p.
Citation
Publisher
Kalamazoo College
License
U.S. copyright laws protect this material. Commercial use or distribution of this material is not permitted without prior written permission of the copyright holder.