## Logic for ApplicationsIn 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 |

409 | |

439 | |

443 | |

### Common terms and phrases

algorithm appears apply atomic formula atomic sentences atomic tableau axiom of choice axiom of extensionality axiom of replacement binary relation cardinals Comp(P completeness theorem consider constant construction contradiction corresponding countable counterexample deduction define definition domain element entry equivalent example Exercise fat herof finished tableau forcing assertion formal formation tree Fp lh frame free variables function symbols given goal clause ground terms Herbrand Herbrand universe Horn clauses induction infinite intuitionistic logic intuitionistically valid labeled language lh tp linear resolution logical consequence mathematics modal logic natural numbers node noncontradictory path notation notion occurs ordinal partial order precisely predicate logic procedure program clauses PROLOG PROLOG program propositional letters propositional logic provable prove quantifiers recursive register machine satisfiable selection rule semantics sequence set theory SLD-tree soundness and completeness structure subset successor Suppose tableau proof Tp lh tp(c true truth table unsatisfiable

### 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.