The inverse method.

*(English)*Zbl 0992.03016
Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier. 179-272 (2001).

From the introduction: There are several methods of theorem proving. The best-known methods are resolution-based and tableau-based ones. Resolution-based methods convert the goal formula into clausal normal form and perform derivation on the set of clauses using a saturation algorithm. Tableau-based methods operate directly on formulas by reducing goals to subgoals and trying to solve the subgoals, either by reduction to new subgoals or by unification-based methods.

The inverse method is much less known. Like the tableau method, it operates on formulas, but the main operation is not reduction of goals to subgoals, but rather construction of goals from previously proved subgoals. Like resolution-based methods, the inverse method uses a saturation algorithm.

The material of this chapter is presented as a small cookbook with recipes. It is organized as follows. In Section 2 we define the main technical notions used in this chapter: those related to multisets and substitutions. In Section 3 we describe how to cook classical logic, based on the Universal Recipe. We define the ingredients for cooking: sequents and sequent calculi, the subformula property necessary for cooking, lifting, and saturation algorithms. In Section 4 we apply the Universal Recipe to nonclassical logics: intuitionistic logic and several modal logics. In Section 5 we discuss the technique of naming and the relation of the inverse method to resolution. To season the calculi, in Section 6 we discuss the notion of redundancy in saturation-based theorem proving. In order to formalize redundancies, in Section 7 we give a new presentation of sequent calculi using the notion of paths in formulas. The use of path calculi simplifies proofs considerably, so we obtain more tasty calculi. We give proofs of completeness for several redundancies for the logic \({\mathbf K}\). In Section 8 we discuss logics without the contraction rule and show that the inverse method gives a decision procedure for first-order versions of such logics. Finally, in Section 9 we discuss the history of the inverse method, the limits of the technique, and possible future research in the area.

For the entire collection see [Zbl 0964.00020].

The inverse method is much less known. Like the tableau method, it operates on formulas, but the main operation is not reduction of goals to subgoals, but rather construction of goals from previously proved subgoals. Like resolution-based methods, the inverse method uses a saturation algorithm.

The material of this chapter is presented as a small cookbook with recipes. It is organized as follows. In Section 2 we define the main technical notions used in this chapter: those related to multisets and substitutions. In Section 3 we describe how to cook classical logic, based on the Universal Recipe. We define the ingredients for cooking: sequents and sequent calculi, the subformula property necessary for cooking, lifting, and saturation algorithms. In Section 4 we apply the Universal Recipe to nonclassical logics: intuitionistic logic and several modal logics. In Section 5 we discuss the technique of naming and the relation of the inverse method to resolution. To season the calculi, in Section 6 we discuss the notion of redundancy in saturation-based theorem proving. In order to formalize redundancies, in Section 7 we give a new presentation of sequent calculi using the notion of paths in formulas. The use of path calculi simplifies proofs considerably, so we obtain more tasty calculi. We give proofs of completeness for several redundancies for the logic \({\mathbf K}\). In Section 8 we discuss logics without the contraction rule and show that the inverse method gives a decision procedure for first-order versions of such logics. Finally, in Section 9 we discuss the history of the inverse method, the limits of the technique, and possible future research in the area.

For the entire collection see [Zbl 0964.00020].

##### MSC:

03B35 | Mechanization of proofs and logical operations |

03F05 | Cut-elimination and normal-form theorems |