DEVELOPMENT OF A PREDICATE LOGIC THEOREM PROVER USING RESOLUTION

Abstract

In conventional datapro'cessing and database appli-cations, knowledge is stored in programs as well as in data-structures. This represents only 'Simple' aspects of some universe. Many knowledge bases will contain large amount of inter-related data and so theori~:s and techniques have to be developed to manage th sE large collection of data. Thus in order to facilitate the expression and just-ification of arguments,various 'formal logies' have been developed. Typically, a formal logic consists of a. a language for expressing knowledge about certain aspects of some universe. b. rules for manipulating formulas expressed in that language. Predicate logic, is one the many representations of 'formal logic'. It allows for expressing specific knowle•d-ge about individuals and also general knowledge about classes of individuals. The syntax of predicate logic language contains 'Predicate Symbols', constants, variables, logical connectives, 'quantifiers' nd functions. One advantage of expressing knowledge as sentences of predicate logic is that generalisations of a class of entities can be expressed conviniently. This is possible through the use of 'quantifiers' . Another advantage is that, 'rules exist which can be used to infer new knowledge from existing knowledge. This thesis di scussEs the development and implemrnt-ation of a tl?eorem - prover of predicate logic. The system allows the user to enter a set of assertions as formulas of r':stricted predicate logic. The system also asks the user to enter the'theorcm' to be proved. The assertions are then tested for consistency and if consistent, the sys-tem goes on to check whether the given theorem. has a 'proof' in the given theory. All formulas are converted to 'clausal form' in this system and 'resolution' is used for reasoning.