RUI: Implementation and Analysis of Proof Techniques Employing Negation Normal Form

这项调查是基于首席研究员以前对否定范式公式结构的分析工作。本工作的结果是路径溶出法的建立。本项目将继续探索该方法及相关推理机制。将进一步发展这一方法的实施，特别是研究以下技术：链接选择；纯规则删除；回溯;理论联系与消解；还有星链。此外，证明理论的问题将被研究，特别是与以下有关：分解，分析表，和分配律；解散与决议；感应和质量。

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.