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.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Application #
9504349
Program Officer
S. Kamal Abdali
Project Start
Project End
Budget Start
1995-09-15
Budget End
1999-08-31
Support Year
Fiscal Year
1995
Total Cost
$151,614
Indirect Cost
Name
University of New Haven
Department
Type
DUNS #
City
West Haven
State
CT
Country
United States
Zip Code
06516