Logic for Applications

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 From the reviews of the second edition: "...the book achieves its goal of being a unified introduction into classical logic, logic programming and certain non-classical logics. ...the book succeeded in presenting a uniform framework for describing different logics. The author's thorough approach to describing logic programming, via introduction of resolution-based refutations and subsequent study of different kinds of resolutions allows the reader to gradually switch from the study of logic to the study of logical programming paradigm and provides a lot of intuition about the behavior of logic programs. As such the book can be recommended both as a textbook for senior/graduate course in logic/logic programming, and as a reading or reference for graduate students in the areas related to discrete mathematics." (Alexander Dekhtyar, William Gasarch's Book Review Column, 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.- 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 andFoundation.- 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.