应用逻辑 第2版PDF电子书下载

Introduction 1

Ⅰ Propositional Logic 7

1 Orders and Trees 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

8 Resolution 49

9 Refining Resolution 62

10 Linear Resolution,Horn Clauses and PROLOG 66

Ⅱ Predicate Logic 81

1 Predicates and Quantifiers 81

2 The Language：Terms and Formulas 83

3 Formation Trees，Structures and Lists 89

4 Semantics：Meaning and Truth 95

5 Interpretations of PROLOG Programs 100

6 Proofs：Complete Systematic Tableaux 108

7 Soundness and Completeness of Tableau Proofs 120

8 An Axiomatic Approach 127

9 Prenex Normsl Form and Skolemization 128

10 Herbrand’s Theorem 133

11 Unification 137

12 The Unification Algorithm 141

13 Resolution 145

14 Refining Resolution：Linear Resolution 153

Ⅲ PROLOG 159

1 SLD-Resolution 159

2 Implementations：Searching and Backtracking 166

3 Controlling the Implementation：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

1 Possibility and Necessity：Knowledge or Belief 221

2 Frames and Forcing 224

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

1 Intuitionism and Constructivism 263

2 Frames and Forcing 265

3 Intuitionistic Tableaux 275

4 Soundness and Completeness 285

5 Decidability and Undecidability 293

6 A Comparative Guide 306

Ⅵ Elements of Set Theory 315

1 Some Basic Axioms of Set Theory 315

2 Boole’8 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 Zermelo-Fraenkel Set Theory in Predicate Logic 345

7 Cardinality：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

Appendix A：An Historical Overview 375

1 Calculus 375

2 Logic 376

3 Leibniz’8 Dream 379

4 Nineteenth Century Logic 380

5 Nineteenth Century Foundatlons 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

10 The Future 395

Appendix B：A Genealogical Database 399

Bibliography 409

Index of Symbols 439

Index ofTerms 443