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 paper ``Tableaux, Path Dissolution, and Decomposable Negation Normal Form for Knowledge Compilation,'' Proceedings of the International Conference TABLEAUX 2003 - Analytic Tableaux and Related Methods, Rome, Italy, September 2003. In Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 2796, 165-180. Additional publications on knowledge compilation are listed below.
(with E. Rosenthal) ``Inference with Path Resolution and Semantic Graphs.'' J.ACM 34,2 (April 1987), 225-254.
(with E. Rosenthal) ``Theory Links: Applications to Automated Theorem Proving.'' Journal of Symbolic Computation 4 (1987), 173-190.
(with E. Rosenthal) ``Dissolution: Making Paths Vanish.'' J.ACM, 40,3 (July 1993), 504-535.
(with E. Rosenthal) ``On the Relative Merits of Path Dissolution and the Method of Analytic Tableaux.'' Theoretical Computer Science, 131 (Aug. 1994), 1-28.
(with E. Rosenthal) ``Adapting Classical Inference Techniques to Multiple-Valued Logics Using Signed Formulas.'' Fundamenta Informaticae Journal, 21,3 (Sept. 1994), 237-253.
(with G. Becker and A. Ramesh) ``CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates.'' Journal of Automated Reasoning, 18,3 (June 1997) 337-356.
(with A. Ramesh, R. Hähnle, and B. Beckert) ``Fast Subsumption Checks Using Anti-Links.'' Journal of Automated Reasoning. 18,1 (Feb. 1997) 47-83.
(with A. Ramesh) ``An Application of Non-Clausal Deduction in Diagnosis.'' Expert Systems with Applications 12,1 (1997), 119-126.
(with J. Lu and E. Rosenthal) ``A Framework for Automated Reasoning in Multiple-Valued Logics.'' Journal of Automated Reasoning, 21,1 (Aug. 1998) 39-67.
(with J. Lu and E. Rosenthal) ``Deduction and Search Strategies for Regular Multiple-Valued Logics.'' Journal of Multiple-Valued Logic and Soft Computing. 11,3-4, (2005), 375-406.
(with R. Hähnle and E. Rosenthal) ``Normal Forms for Knowledge Compilation.'' Proceedings of the International Symposium on Methodologies for Intelligent Systems, (ISMIS `05, Z. Ras ed.), Lecture Notes in Computer Science, Springer, Vol. 3488, 304-313.
(with E. Rosenthal) ``Duality in Knowledge Compilation Techniques.'' Proceedings of the International Symposium on Methodologies for Intelligent Systems, (ISMIS `05, Z. Ras ed.), Lecture Notes in Computer Science, Springer, Vol. 3488, 182-190.
(with E. Rosenthal) ``Efficient Query Processing with Reduced Implicate Tries.'' Journal of Automated Reasoning 38,1-3 (2007), 155-172.
(with E. Rosenthal) ``Reduced Implicate Tries with Updates.'' Journal of Logic and Computation, 20, 261-281, (2010).
(with E. Rosenthal) ``Linear Response Time for Implicate and Implicant Queries.'' Knowledge and Information Systems. 22, 3 (2010) 287-317.
(with E. Rosenthal) ``Identifying Prime Implicate Branches in ri-Tries.'' Fundamenta Informaticae. 99,2 (2010) 227-243.
(with A. Matusiewicz, Paul Olsen, and E. Rosenthal) ``Computing Prime Implicates by Pruning the Search Space and Accelerating Subsumption.'' Journal of Logic and Computation. 25,6 (December 2015). (Submitted version)