This project is for research in computational logic. The areas of research stem directly from prior analysis of the structure formulas in negation normal form. That work raised many questions and led to explorations in several directions. Substantial results at the propositional level, preliminary experimental at the first order level, and certain theoretical results that the most important of these may be path dissolution, a rule of inference that is strongly complete at the ground level. This project continues exploration of this and related inference mechanisms, largely through experimentation. One major thrust is to further the implementation of the techniques developed earlier. The current first order system (``Dissolver'') is a solid platform on which the following techniques may 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, enhancing the performance of Dissolver is an important motivation for the theoretical work in this project. The investigations into multiple-valued logics largely fit the category; the study of the following issues contributes to the development of Dissolver: dissolution and multiple-valued logics; dissolution, analytic tableaux, and distributive law; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.
