This is a research project in computational logic. The areas of research stem directly from the analysis of the structure of formulas in negation toward several research topics. Substantial experimental results at the propositional level, preliminary experimental results at the first order level, and certain theoretical results indicate that the most important of these may be path dissolution, a rule of inference that is strongly complete at the ground level. Exploration of this and related inference mechanisms will be continued, largely through experimentation. One major thrust of the investigation will be to further the implementation of the path resolution and semantic graph techniques developed earlier. A sophisticated ground system and a first order system are now operational; the latter is a solid platform on which techniques proposed below will be tested: link selection; computing prime implicants; backtracking; theory links and dissolution; and star chains. While abstract proof-theoretic questions are of interest in their own right, the development of performance enhancements for the theorem proving system is also a major motivation. A number of such enhancements will be investigated. Among them are: improved efficiency of existing inference mechanisms; improved proof search with existing mechanisms; and development of new inference techniques that alter the search space itself. Specifically, system development will be enhanced through investigation of: dissolution, analytic tableaux, and the distributive law; dissolution versus resolution; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.
