Logic for Applications

Front Cover
Springer Science & Business Media, Feb 1, 1997 - Computers - 456 pages
1 Review
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

Common terms and phrases

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.

References to this book

All Book Search results »

About the author (1997)

Anil Nerode is Professor and Director of the Mathematical Sciences Institute at Cornell University.

Shore was commissioned (Major) Armor from Worcester Polytechnic Institute in 1984. He is a decorated officer. He has held numerous Operational and Joint Staff assignments and is a graduate of the Army Resident and non-resident Command and General Staff Colleges, The Naval Command and Staff College and is currently enrolled in the Air Force Command and General Staff College. He has a Bachelor's degree in Business Administration.