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