数理逻辑引论与归结原理

Preface
Chapter 1 Preliminaries
1．1 Partially ordered sets
1．2 Lattices
1．3 Boolean algebras

Chapter 2 Propositional Calculus
2．1 Propositions and their symbolization
2．2 Semantics of propositional calculus
2．3 Syntax of propositional calculus

Chapter 3 Semantics of First Order Predicate Calculus
3．1 First order languages
3．2 Interpretations and logically valid formulas
3．3 Logical equivalences

Chapter 4 Syntax of First Order Predicate Calculus
4．1 The formal system KL
4．2 Provable equivalence relations
4．3 Prenex normal forms
4．4 Completeness of the first order system KL
*4．5 Quantifier-free formulas

Chapter 5 Skolem's Standard Forms and Herbrand's Theorems
5．1 Introduction
5．2 Skolem standard forms
5．3 Clauses
*5．4 Regular function systems and regular universes
5．5 Herbrand universes and Herbrand's theorems
5．6 The Davis-Putnam method

Chapter 6 Resolution Principle
6．1 Resolution in propositional calculus
6．2 Substitutions and unifications
6．3 Resolution Principle in predicate calculus
6．4 Completeness theorem of Resolution Principle
6．5 A simple method for searching clause sets S

Chapter 7 Refinements of Resolution
7．1 Introduction
7．2 Semantic resolution
7．3 Lock resolution
7．4 Linear resolution

Chapter 8 Many-Valued Logic Calculi
8．1 Introduction
8．2 Regular implication operators
8．3 MV-algebras
8．4 Lukasiewicz propositional calculus
8．5 R0-algebras
8．6 The propositional deductive system L*

Chapter 9 Quantitative Logic
9．1 Quantitative logic theory in two-valued propositional logic system L
9．2 Quantitative logic theory in L ukasiewicz many-valued propositional logic systems Ln and Luk
9．3 Quantitative logic theory in many-valued R0-propositional logic systems L*n and L*
9．4 Structural characterizations of maximally consistent theories
9．5 Remarks on Godel and Product logic systems
Bibliography
Index