Logic for Applications

This textbook provides a first introduction to mathematical logic which is closely attuned to the applications of logic in computer science. In it the authors emphasize the notion that deduction is a form of computation. Whilst all the traditional subjects of logic are covered thoroughly: syntax, semantics, completeness, and compactness; much of the book deals with less traditi...

(展开全部)

This textbook provides a first introduction to mathematical logic which is closely attuned to the applications of logic in computer science. In it the authors emphasize the notion that deduction is a form of computation. Whilst all the traditional subjects of logic are covered thoroughly: syntax, semantics, completeness, and compactness; much of the book deals with less traditional topics such as resolution theorem proving, logic programming and non-classical logics - modal and intuitionistic - which are becoming increasingly important in computer science. No previous exposure to logic is assumed and so this will be suitable for upper level undergraduates or beginning graduate students in computer science or mathematics. From reviews of the first edition: "...must surely rank as one of the most fruitful textbooks introduced into computer science ...We strongly suggest it as a textbook ..." SIGACT News

I Propositional Logic
1 Orders and Trees
2 Propositions, Connectives and Truth Tables
3 Truth Assignments and Valuations
4 Tableau Proofs in Propositional Calculus
5 Soundness and Completeness of Tableau Proofs
· · · · · · (更多)

I Propositional Logic
1 Orders and Trees
2 Propositions, Connectives and Truth Tables
3 Truth Assignments and Valuations
4 Tableau Proofs in Propositional Calculus
5 Soundness and Completeness of Tableau Proofs
6 Deductions from Premises and Compactness
7 An Axiomatic Approach*
8 Resolution
9 Refining Resolution
10 Linear Resolution, Horn Clauses and PROLOG
II Predicate Logic
1 Predicates and Quantifiers
2 The Language: Terms and Formulas
3 Formation Trees, Structures and Lists
4 Semantics: Meaning and Truth
5 Interpretations of PROLOG Programs
6 Proofs: Complete Systematic Tableaux
7 Soundness and Completeness of Tableau Proofs
8 An Axiomatic Approach*
9 Prenex Normal Form and Skolemization
10 Herbrand’s Theorem
11 Unification
12 The Unification Algorithm
13 Resolution
14 Refining Resolution: Linear Resolution
III PROLOG
1 SLD-Resolution
2 Implementations: Searching and Backtracking
3 Controlling the Implementation: Cut
4 Termination Conditions for PROLOG Programs
5 Equality
6 Negation as Failure
7 Negation and Nonmonotonic Logic
8 Computability and Undecidability
IV Modal Logic
1 Possibility and Necessity; Knowledge or Belief
2 Frames and Forcing
3 Modal Tableaux
4 Soundness and Completeness
5 Modal Axioms and Special Accessibility Relations
6 An Axiomatic Approach*
V Intuitionistic Logic
1 Intuitionism and Constructivism
2 Frames and Forcing
3 Intuitionistic Tableaux
4 Soundness and Completeness
5 Decidability and Undecidability
6 A Comparative Guide
VI Elements of Set Theory
1 Some Basic Axioms of Set Theory
2 Boole’s Algebra of Sets
3 Relations, Functions and the Power Set Axiom
4 The Natural Numbers, Arithmetic and Infinity
5 Replacement, Choice and Foundation
6 Zermelo-Fraenkel Set Theory in Predicate Logic
7 Cardinality: Finite and Countable
8 Ordinal Numbers
9 Ordinal Arithmetic and Transfinite Induction
10 Transfinite Recursion, Choice and the Ranked Universe
11 Cardinals and Cardinal Arithmetic
Appendix A: An Historical Overview
1 Calculus
2 Logic
3 Leibniz’s Dream
4 Nineteenth Century Logic
5 Nineteenth Century Foundations of Mathematics
6 Twentieth Century Foundations of Mathematics
7 Early Twentieth Century Logic
8 Deduction and Computation
9 Recent Automation of Logic and PROLOG
10 The Future
Appendix B: A Genealogical Database
Index of Symbols
Index of Terms
· · · · · · (收起)