This investigation is based on the principal investigator's previous work on the analysis of the structure of formulas in negation normal form. A result of this work was the formulation of the path dissolution method. This project will continue exploration of this method and related inference mechanisms. The implementation of this method will be developed further to investigate the following techniques in particular: link selection; pure rule deletion; backtracking; theory links and dissolution; and star chains. Also, proof-theoretic questions will be studied, in particular, related to the following: dissolution, analytic tableaux, and the distributive law; dissolution vs. resolution; induction and quality.
