Guo-Jun Wang、Hong-Jun Zhou著的《數理邏輯
引論與歸結原理(英文版）（精）》在第一版的基礎
上進行修訂再版，全書共9章，內容可分為Boole代數
理論，命題演算與謂詞演算理論，歸結原理理論，多
值邏輯的最新理論等4部分。同時，在第一版的基礎
上對“計量邏輯學”，關於一階繫統K完備性的證明
等諸多內容做了補充或改寫。
本書可供計算機專業、應用數學專業、人工智能
專業的研究生與高年級本科生及教師閱讀。

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