This research focuses on extending logic programming beyond first order logic. One kind ofextension allows more kinds of clauses in the knowledge base. In particular, indefinite clauses are allowed to exist in the knowledge base, and processing strategies are developed so that inference takes not significantly longer than a multiple of the time required in the case of definite clauses only. A second extension permits the use of variables in place of predicate and function symbols in definite clauses. The importance of this work is in developing automatic program transformation and verification systems, and in illuminating the fundamental processes required for logic programming in knowledge based systems.
