The main current application of automated deduction is to a knowledge base and a query “Q?”. The system gives the answer “yes” if and only if Q can be deduced from the knowledge base. The inference engines are mainly based on resolution and other methods originally developed for classical logic. Important situations exist, however, when we need automated deduction for nonclassical logics. For example, our knowledge may contain not only affirmative statements but also statements saying that something is possible or necessary; to express these statements we have to use some version of modal logic, and to answer queries for such knowledge bases we have to develop methods of automated deduction for modal logics. Classical logic is also insufficient for constructive knowledge, which expresses not only what an expert knows but also what she or he can do, such as “I can solve problem A” or “if I can solve A then I can solve B.” The appropriate formalism for these statements is intuitionistic logic. If the knowledge base describes everything that we can compute, the answer to a query of the type “Can we compute Q?” is positive if and only if the statement “We can compute Q” can be deduced from our knowledge by using intuitionistic logic. These examples show that we need automated deduction for nonclassical logics.

The common approach to this problem is that resolution works so well for classical logic that we should try to adapt it for other logics. The main disadvantage of this approach is that classical resolution is based on the reduction to normal form, which is impossible in other logics. Some tricks have been invented to overcome this difficulty, but the resulting modifications of the resolution method are not natural and therefore are less efficient than the original resolution method. Also, many important nonclassical logics exist (including several versions of modal logic), and even when we know a trick for one of them it does not help us deal with the others. The author therefore tries to find a general approach to all these logics.

He starts with the question, “Why is automated deduction possible for these logics?” No matter what rules we have, we can present an “algorithm” by generating all possible deductions until we find Q, but this procedure takes exponential time and is meaningless. What makes automated deduction really possible is that in all the reasonable logics, we can restrict the deduction rules so that all the formulas used in a deduction of Q must be somehow connected with Q. For example, all the statements used in the deduction of the sequent K→Q must be subformulas of formulas from this sequent. This fact leads to an algorithm for automated deduction: given a proposition, find one or more sequents from which it could be deduced using one of the rules (the new sequents consist of appropriate subformulas of the original formulas), find the sequents from which these could be obtained, and repeat this procedure until a deduction is found. This algorithm is generally extremely redundant. First, notations are redundant: every new formula is a subformula of an already-written formula, so it contains large blocks in common with the original formula, but we have to rewrite these blocks at each step. Second, this algorithm sometimes spends too much time on irrelevant things. If we try to prove A,B&C→C, where A, B, and C are expressions, then we have a choice as to which of the complicated formulas A, B&C, and C to reduce first. If we always reduce the leftmost formula first then we will spend a lot of time on disclosing an irrelevant formula A. The third source of redundancy is that some rules are commutative: for instance, if we prove A&B, it does not matter whether we first prove A or B, but formally, when we look for a proof in the above manner, we must consider both possible deductions although practically they are the same.

To overcome these redundancies, the author uses Bibel and Andrews’s representation of a formula by a graph of its possible subformulas. Deduction can be described as a path through these graphs. We do not have to rewrite the common blocks: it is sufficient to indicate the values of the parameters of the corresponding subformulas (for example, t if F ( t ) is a subformula of ( ∃ x ) F ( x ). The second type of redundancy disappears because when choosing a path we can first check whether any of its subformulas are relevant, and the third type vanishes because two commutative rules lead to the same subformula. Wallen begins by providing the corresponding formalism and proof-search strategies for classical logics. He then uses the Kripke-model translation of modal logic into first-order logic with variables for possible worlds, where “necessary” means “for all possible worlds” and “possible” means existence, to generalize this approach to modal logics. Godel’s embedding of the intuitionistic logic J into the modal logic S4 is used as a hint to generalize this approach to J. Wallen analyzes the existing methods of automated deduction from this viewpoint; known tricky modifications of resolution turn out to be natural cases of this general scheme.

The author’s algorithms are not ideal (he himself shows where they can be improved), but he does present a general formalism that can also be used to generalize different versions of resolution and other automated deduction ideas to nonclassical logics, including modal and intuitionistic logics. This monograph is aimed at researchers rather than students. The approach is promising and the book is worth reading.