应用逻辑：第2版

"Preface

Introduction

IPropositionalLogic

1OrdersandTrees

2Propositions,ConnectivesandTruthTables

3TruthAssignmentsandValuations

4TableauProofsinPropositionalCalculus

5SoundnessandCompletenessofTableauProofs

6DeductionsfromPremisesandCompactness

7AnAxiomaticApproach*

8Resolution

9RefiningResolution

10LinearResolution,HornClausesandPROLOG

IIPredicateLogic

1PredicatesandQuantifiers

2TheLanguage:TermsandFormulas

3FormationTrees,StructuresandLists

4Semantics:MeaningandTruth

5InterpretationsofPROLOGPrograms

6Proofs:CompleteSystematicTableaux

7SoundnessandCompletenessofTableauProofs

8AnAxiomaticApproach*

9PrenexNormalFormandSkolemization

10Herbrand’sTheorem

11Unification

12TheUnificationAlgorithm

13Resolution

14RefiningResolution:LinearResolution

IIIPROLOG

1SLD-Resolution

2Implementations:SearchingandBacktracking

3Controllingtheimplementation:Cut

4TerminationConditionsforPROLOGPrograms

5Equality

6NegationasFailure

7NegationandNonmonotonicLogic

8ComputabilityandUndecldability

IVModalLogic

1POssibilityandNecessity;KnowledgeorBelief

2FramesandForcing

3ModalTableaux

4SoundnessandCompleteness

5ModalAxiomsandSpecialAccessibilityRelations

6AnAxiomaticApproach*

VIntultionistlcLogic

1IntuitionismandConstructivism

2FramesandForcing

3IntuitionisticTableaux

4SoundnessandCompleteness

5DecidabilityandUndecidability6AComparativeGuide

VIElementsofSetTheory

1SomeBasicAxiomsofSetTheory

2Boole’sAlgebraofSets

3Relations,FunctionsandthePowerSetAxiom

4TheNaturalNumbers,ArithmeticandInfinity

5Replacement,ChoiceandFoundation

6Zermelo-FraenkelSetTheoryinPredicateLogic

7Cardinality:FiniteandCountable

8OrdinalNumbers

9OrdinalArithmeticandTransfiniteInduction

10TransfiniteRecursion,ChoiceandtheRankedUniverse

11CardinalsandCardinalArithmetic

AppendixA:AnHistoricalOverview

1Calculus

2Logic

3Leibniz’sDream

4NineteenthCenturyLogic

5NineteenthCenturyFoundationsofMathematics

6TwentiethCenturyFoundationsofMathematics

?EarlyTwentiethCenturyLogic

8DeductionandComputation

9RecentAutomationofLogicandPROLOG

10TheFuture

AppendixB：AGenealogicalDatabase

Bibliography

IndexofSymbols

IndexofTerms

"

"　　这是一本结合逻辑在计算机科学中的应用来介绍数理逻辑的教科书，书中强调了演绎作为计算的一种形式的概念。虽然本书覆盖了所有传统的逻辑主题(语法、语义、完备性和紧致性)，但是书中大部分讨论的是其他主题，诸如消解定理证明、逻辑式程序设计和非经典逻辑(模态逻辑和直觉主义逻辑)，而这些主题在现代计算机科学中变得越来越重要。另外，本书还系统介绍了集合论基础知识，并对该主题提供了历史综述。 本书不要求读者具备逻辑基础知识，适合计算机科学和数学系高年级本科生以及低年级研究生使用。　　This book is a rigorous elementary introduction to classical predicate logic emphasizing that deduction is a form of computation. We cover the standard topics of soundness, completeness and compactness: our proof methods produce only valid results, all valid sentences are provable and, if a fact is a logical consequence of an infinite set of axioms, it is actually a consequence of finitely many of them. The need for soundness seems obvious but, as we see in our discussion Of PROLOG, even this requirement of simple correctness is often sacrificed on the altar of efficiency in actual implementations. Completeness, on the other hand, is a remarkable result connecting proofs and validity. We can prescribe an effective proof procedure that precisely captures the semantics of first order logic. A valid sentence, i.e., one true for every interpretation of the relations used to state it, always has a proof in a particular formal system and there is an algorithm to find such a proof. Compactness also has surprising applications that deduce results about infinite structures from results about finite ones. To cite just one example, it implies that every planar map is colorable with four colors as every finite planar map is so colorable. We also prove that validity is undecidable: no single algorithm can decide if any given sentence is valid. Thus, although we can, using a particular algorithm, search for a proof of a given sentence φ and be assured of finding one if φ is valid, we cannot know in general whether we are searching in vain."