Abstract
Two related but independent topics are treated dealing with methods for mechanical theorem proving in the first order predicate calculus using the resolution system of J. A. Robinson. Current research efforts are almost totally oriented towards reducing the amount of effort required by existing methods to and this thesis is a relating to efficiency. The first topic of the thesis deals with a new strategy, called Hereditary Lock Resolution (HLR) which is a refinement of the original resolution inference rule. HLR is composed of two interacting refinements. One is a modification of the locking refinement (a syntactic refinement) of Boyer, and the other is a strengthening of the model strategy (a semantic refinement) of Luckham. Previously known strategies combining syntactic and semantic components either used a weaker syntactic strategy than lock resolution, or used weaker semantic notions, incomplete ( i -e -unable to prove complete and sound (i.e. never constructs some theorems).or were HLR is fallacious proofs). HLR generates a search space involving clauses, as does ordinary resolution, but each clause has attached to it an additional data structure which contains information about the deduction leading to that clause. This data structure is called an PSL (False Substitution List) and consists of a set of literals all of which must be falsifiable according to some model (which initially can be chosen arbitrarily) - The FSL mechanism is applicable to other semantic refinements of resolution besides HLR, and this is illustrated specifically for the case of the model strategy of Luckham. The second topic of the specification and use of models interpretation, concerns the thesis in resolution inference systems. The usual requirement in semantic refinements of resolution has been that the model used must be a Herbrand which is an abstractly defined way of considering models. However, in pragmatic situations where implemented procedures must utilize models, Herbrand interpretations which capture the relevant structure of the doma-in to be modeled usually are both difficult to find and computationally costly to use. The thesis takes the position that the essence of the difficulty is that Herbrand interpretations require the specification of details which are mostly irrelevant to the theorem proving task, and that the way out of this difficulty is to develop a theory of models which are based on incomplete specification. The key to doing this is to focus on the interface between a semantic refinement of resolution (e.g. HLR) and the model. This interface is simple and is adequately summarized by the notion of a semantic function, which is a function mapping logical sentences into the values "true" or "false". Once this is done a simple theory of incompletely specified models can be developed which defines semantic functions with the appropriate properties. The theory is both simple enough and detailed enough so that completeness of HLR and other semantic refinements can be demonstrated using these semantic functions instead of the usual Herbrand interpretations. The efficiency problem in first order mechanical theorem proving is a multifaceted and difficult issue, and the results and views presented in this thesis are to be considered not as final solutions, but instead as contributions to the perspective and knowledge base from which more adequate strategies will ultimately be formulated.