This book is a revised version of my PhD. dissertation submitted to the Dept. of Artificial Intelligence, University of Edinburgh, Scotland, under the supervision of Prof. Alan Bundy.
Although Leibniz' seventeenth-century dream of a symbolic language for the representation and mechanical solution of all scientific and mathematical problems has suffered at the hands of the undecidability, incompleteness and independence results of modern mathematical logic, the spirit of his idea lives on within Computing Science. 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.
Author(s): Lincoln A. Wallen
Publisher: The MIT Press
Year: 1990
Language: English
Pages: 252
Contents ......Page 4
List of figures ......Page 6
List of tables ......Page 8
Series foreword ......Page 9
Acknowledgements ......Page 10
Introduction ......Page 11
PART I. CLASSICAL LOGIC ......Page 15
Introduction to Part I ......Page 17
§1. Syntax and semantics ......Page 19
§2. The sequent calculus ......Page 22
§3. Search methods ......Page 26
§4. Redundancy in the sequent search space ......Page 31
§1. Introduction ......Page 39
§2. Formula trees and notational redundancy ......Page 42
§3. Paths, connections and irrelevance ......Page 54
§4. Reduction orderings and permutability ......Page 60
PART II. MODAL LOGIC ......Page 67
Introduction to Part II ......Page 69
§1. Syntax, semantics and notation ......Page 71
§2. Sequent calculi for modal logics ......Page 77
§3. S5 and constant domain modal logics ......Page 89
§1. Introduction ......Page 92
§2. Notational redundancy and relevance ......Page 93
§3. Non-permutability ......Page 95
§4. Interactions: modal operators and quantifiers ......Page 97
§1. Introduction ......Page 101
§2. Matrices, paths and connections ......Page 106
§3. Correctness ......Page 129
§4. Completeness ......Page 155
§2. Unification problems ......Page 164
§3. Proof search in the matrix systems ......Page 170
§4. Decision procedures ......Page 186
§5. Logical consequence and expressibility ......Page 196
§1. Introduction ......Page 198
§2. Sequent and tableau-based proof systems ......Page 199
§3. Resolution-based proof systems ......Page 201
§4. Hybrid systems ......Page 207
PART III. INTUITIONISTIC LOGIC ......Page 211
Introduction to Part III ......Page 213
§4. Introduction ......Page 215
§2. Kripke semantics for J ......Page 216
§3. A cut-free sequent calculus for J ......Page 217
§4. A matrix characterisation of validity in J ......Page 220
§5. Correctness and completeness ......Page 231
§6. Alternative proof methods ......Page 233
§7. Summary ......Page 234
Conclusion ......Page 235
Bibliography ......Page 238
Index of symbols ......Page 245
Index ......Page 246
