My main research interest is in automated deduction; this has included both theoretical and experimental studies. The development of inference techniques for negation normal form (NNF) formulas and related tableau-based techniques is central. These techniques are relevant not only for automated theorem provers, but for other systems; examples are deductive databases, systems based on logic programming, and other AI systems with an inferencing component such as deduction-based program synthesis and non-monotonic reasoning systems.
NNF-based techniques are also promising for producing a representation of the models of a (propositional) formula. This capability is important for many more practical applications than was previously thought to be the case. Planning is one example, and fault-diagnosis is another. These issues are closely related to recent developments in ``Decomposable Negation Normal Form (DNNF)'' (Darwiche, J.ACM (48,4), July 2001), and to our forthcoming paper ``Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation,'' to appear in the Proceedings of the International Conference TABLEAUX 2003 - Analytic Tableaux and Related Methods, Rome, Italy, September 2003 (see N.V. Murray and E. Rosenthal. ``Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation.'' Technical Report 03-3, Dept. of Computer Science, University at Albany - SUNY, March 2003).
"Inference with Path Resolution and Semantic Graphs." J.ACM 34,2 (April 1987), 225-254.
"Theory Links: Applications to Automated Theorem Proving." Journal of Symbolic Computation 4 (1987), 173-190.
"Dissolution: Making Paths Vanish." J.ACM, 40,3 (July 1993), 504-535.
"On the Relative Merits of Path Dissolution and the Method of Analytic Tableaux." Theoretical Computer Science, 131 (Aug. 1994), 1-28.
"Adapting Classical Inference Techniques to Multiple-Valued Logics Using Signed Formulas." Fundamenta Informaticae Journal, 21,3 (Sept. 1994), 237-253.
"CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates." Journal of Automated Reasoning, 18,3 (June 1997) 337-356.
Fast Subsumption Checks Using Anti-Links. Journal of Automated Reasoning. 18,1 (Feb. 1997) 47-83. .
"An Application of Non-Clausal Deduction in Diagnosis." Expert Systems with Applications 12,1 (1997), 119-126.
"A Framework for Automated Reasoning in Multiple-Valued Logics." Journal of Automated Reasoning, 21,1 (Aug. 1998) 39-67.
``Deduction and Search Strategies for Regular Multiple-Valued Logics.'' To appear in Journal of Multiple-Valued Logic and Soft Computing.