# Logic for Applications

Springer Science & Business Media, Jan 17, 1997 - Computers - 456 pages
In writing this book, our goal was to produce a text suitable for a first course in mathematical logic more attuned than the traditional textbooks to the re cent dramatic growth in the applications oflogic to computer science. Thus, our choice oftopics has been heavily influenced by such applications. Of course, we cover the basic traditional topics: syntax, semantics, soundnes5, completeness and compactness as well as a few more advanced results such as the theorems of Skolem-Lowenheim and Herbrand. Much ofour book, however, deals with other less traditional topics. Resolution theorem proving plays a major role in our treatment of logic especially in its application to Logic Programming and PRO LOG. We deal extensively with the mathematical foundations ofall three ofthese subjects. In addition, we include two chapters on nonclassical logics - modal and intuitionistic - that are becoming increasingly important in computer sci ence. We develop the basic material on the syntax and semantics (via Kripke frames) for each of these logics. In both cases, our approach to formal proofs, soundness and completeness uses modifications of the same tableau method in troduced for classical logic. We indicate how it can easily be adapted to various other special types of modal logics. A number of more advanced topics (includ ing nonmonotonic logic) are also briefly introduced both in the nonclassical logic chapters and in the material on Logic Programming and PROLOG.

### What people are saying -Write a review

User Review - Flag as inappropriate

The material covered by this book is straight forward - however, you would only realize this if you learned mathematical logic prior to using this book. It is difficult to understand and phrased poorly.

### Contents

 Introduction 1 Propositional Logic 7 2 Propositions Connectives and Truth Tables 12 3 Truth Assignments and Valuations 23 4 Tableau Proofs in Propositional Calculus 27 5 Soundness and Completeness of Tableau Proofs 38 6 Deductions from Premises and Compactness 40 7 An Axiomatic Approach 47
 3 Modal Tableaux 228 4 Soundness and Completeness 239 5 Modal Axioms and Special Accessibility Relations 249 6 An Axiomatic Approach 259 Intuitionistic Logic 263 2 Frames and Forcing 265 3 Intuitionistic Tableaux 275 4 Soundness and Completeness 285

 8 Resolution 49 9 Refining Resolution 62 10 Linear Resolution Horn Clauses and PROLOG 66 Predicate Logic 81 Terms and Formulas 83 3 Formation Trees Structures and Lists 89 Meaning and Truth 95 5 Interpretations of PROLOG Programs 100 Complete Systematic Tableaux 108 7 Soundness and Completeness of Tableau Proofs 120 8 An Axiomatic Approach 127 9 Prenex Normal Form and Skolemization 128 10 Herbrands Theorem 133 11 Unification 137 12 The Unification Algorithm 141 13 Resolution 145 Linear Resolution 153 PROLOG 159 Searching and Backtracking 166 Cut 178 4 Termination Conditions for PROLOG Programs 182 5 Equality 188 6 Negation as Failure 192 7 Negation and Nonmonotonic Logic 203 8 Computability and Undecidability 211 Modal Logic 221 2 Frames and Forcing 224
 5 Decidability and Undecidability 293 6 A Comparative Guide 306 Elements of Set Theory 315 2 Booles Algebra of Sets 318 3 Relations Functions and the Power Set Axiom 321 4 The Natural Numbers Arithmetic and Infinity 328 5 Replacement Choice and Foundation 339 6 ZermeloFraenkel Set Theory in Predicate Logic 345 Finite and Countable 348 8 Ordinal Numbers 354 9 Ordinal Arithmetic and Transfinite Induction 360 10 Transfinite Recursion Choice and the Ranked Universe 364 11 Cardinals and Cardinal Arithmetic 368 An Historical Overview 375 2 Logic 376 3 Leibnizs Dream 379 4 Nineteenth Century Logic 380 5 Nineteenth Century Foundations of Mathematics 383 6 Twentieth Century Foundations of Mathematics 387 7 Early Twentieth Century Logic 389 8 Deduction and Computation 392 9 Recent Automation of Logic and PROLOG 395 A Genealogical Database 399 Bibliography 409 Index of Symbols 439 Index of Terms 443 Copyright

### Popular passages

Page 426 - Lambek, J. and Scott, PJ Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, 1986. [15] Landin, PJ "A correspondence between ALGOL 60 and Church's lambda notation".
Page 426 - First order categorical logic. — Modeltheoretical methods in the theory of topoi and related categories.
Page 435 - Nonmonotonic Reasoning: Logical Foundations of Commonsense. Cambridge University Press, Cambridge, England, 1991.