Logic for applications = 应用逻辑 / 2nd ed.

preface

introduction.

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

bibliography

index of symbols

index of terms...