This monograph is an attempt to investigate logical systems and their resolution proof systems using a unified abstract algebra–based framework. The book deals with automated reasoning programs in the context of nonclassical reasoning. It presents an algebraic theory of resolution proof systems and points out the potential of this formal algebraic approach for constructing and analyzing resolution-based automated reasoning programs.

The book consists of eight chapters and six appendices. The basics of propositional and first-order logics are presented briefly in the first chapter. Two important notions in the theory of resolution proof systems are introduced next, namely, the notion of a propositional resolution proof system viewed as a deductive proof system, which is essentially based on the nonclausal form of the resolution principle, and the notion of a propositional resolution logic.

The class of propositional resolution logics is characterized in the third chapter. The resolution counterparts of disjunctive logics and results concerning the effects of disjunctions on the deductive process are also presented here. Several ways of minimizing the number of verifiers in the resolution rule, mainly focused on minimizing the length of resolvents and simplifying the termination test, are discussed in the fourth chapter. The efficiency of resolution-based reasoning programs depends on the ability to control the number of applications of the resolution rule during the deductive process. The fifth chapter is devoted to speed-up techniques for controlling and directing the deductive process. Two such techniques, the support strategy and the polarity strategy, are presented in detail. The next chapter introduces resolution circuits as multiresolution proof system representations of resolution logics. The theory of propositional resolution proof systems is extended to finite-valued first-order logics in chapter 7. Nonmonotonic inference systems arose as a result of the search for logical tools that can handle a variety of forms of reasoning involving inferences based on information that is incomplete, uncertain, approximate, or subject to revision. The final chapter presents a possible way of extending the resolution proof system methodology developed so far to cumulative nonmonotonic inference systems.

This monograph on a theory of resolution proof systems is particularly suitable as a reference book for researchers and as a textbook for graduate courses on the theoretical aspects of automated reasoning and computational logic.