zbMATH — the first resource for mathematics

Automated proof search in non-classical logics. Efficient matrix proof methods for modal and intuitionistic logics. (English) Zbl 0782.03003
MIT Press Series in Artificial Intelligence. Cambridge: MIT Press. xvi, 239 p. (1990).
From the introduction: “It has proved practical to solve problems mechanically by testing sentences of a symbolic logic for theoremhood using a computer, even though the decision problem for the logic might be technically intractable. The practical performance of algorithms for such automated deduction – or automated proof search – can be improved by standard optimisation techniques, novel data structures and more powerful hardware, but in the final analysis successful algorithms arise from computationally sensitive characterisations of the logics themselves.”
“In this book a number of such computationally sensitive characterisations are developed for various first-order logics. The aim has been to lay the groundwork for a theory of automated deduction in arbitrary symbolic logics by providing empirical evidence for the existence of a uniform approach to efficient proof search in both truth- functional and non truth-functional logics. Whilst the formulation of such a comprehensive theory is at the time of writing beyond the author’s reach, it is intended that the form such a theory might take, and the ideas on which it might be based, be suggested by the methods brought to bear in the text.”
“The central theme is that of a matrix characterisation. Such a characterisation involves a geometrical view of formulae as two- dimensional structures or matrices. The associated notion of a path through a matrix gives rise to a natural notion of path through a formula and then to the idea of a connection: two elements (subformulae) of the matrix (formula) on such a path that are complementary in some fashion. Theoremhood is expressed in terms of (the existence of) a set of simultaneously complementary connections that spans the formula; the latter condition ensuring that every path contains a connection from the set.”
“In this way testing for theoremhood is reduced to path-checking in a matrix. Algorithms for this task may be developed independently of a given logic and are parameterised in terms of the definition of complementarity.”
Contents: Part I. Classical logic (1. Proof search in classical sequent calculi; 2. Matrix characterisation of classical logic). Part II. Modal logic (3. Semantics and proof theory of modal logics; 4. Proof search in modal sequent calculi; 5. Matrix characterisation of modal logics; 6. Matrix-based proof search; 7. Alternative proof methods). Part III. Intuitionistic logic (8. A matrix characterisation).

03B35 Mechanization of proofs and logical operations
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
68-02 Research exposition (monographs, survey articles) pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B10 Classical first-order logic
03B20 Subsystems of classical logic (including intuitionistic logic)
03B45 Modal logic (including the logic of norms)
03F05 Cut-elimination and normal-form theorems