书籍详情
面向计算机科学的数理逻辑：系统建模与推理 英文版
作者：（英）Michael Huth，（英）Mark Ryan著
出版社：机械工业出版社
出版时间：2005-04-01
ISBN：9787111160533
定价：¥49.00
购买这本书可以去
内容简介
数理逻辑是计算机科学的基础之一，在模型与系统的规约与验证等方面有着广泛的应用。随着当今软硬件产品（电路、程序和通信协议等）日趋复杂，数理逻辑已经成为越来越多设计开发人员的日常工具。本书适合作为高等院校计算机及相关专业的数理逻辑／形式化方法课程教材，涵盖了命题逻辑、谓词逻辑、模态逻辑与Agent、二元决策图、模型检查和程序验证等内容。与传统数理逻辑教科书相比，它的主要特色就是紧紧围绕软硬件规约和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性（SAT）算法、紧致性理论和Lowenheim-Skolem定理，并介绍了Alloy语言和NuSMV工具。本书自出版以来受到广泛好评，已经被包括美国普林斯顿大学、卡内基—梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰Vrije大学、印度理工学院在内的多个国家几十所高校采纳为教材。
作者简介
MichaelHuth，伦敦帝国学院计算机系高级讲师，研究方向包括模型检测与抽象，程序分析和模型检测中有序结构的应用等。相关图书软件过程改进（英文版）80X86汇编语言与计算机体系结构计算机科学概论（英文版·第2版）分布式系统概念设计调和分析导论（英文第三版）人工智能：智能系统指南（英文版）第二版电力系统分析（英文版·第2版）Java2专家导引（英文版·第3版）支持向量机导论（英文版）电子设计自动化基础（英文版）Java教程（英文版·第2版）软件需求管理：用例方法（英文版·第2版）数字通信导论离散事件系统仿真（英文版·第4版）复杂SoC设计（英文版）基于FPGA的系统设计（英文版）UML参考手册（英文版·第2版）计算理论导引实用软件工程（英文版）计算机取证（英文版）EffectiveC#（英文版）基于用例的面向方面软件开发（英文版）Linux内核编程必读-经典原版书库实分析和概率论-经典原版书库（英文版.第2版）计算机体系结构：量化研究方法：第3版数学规划导论英文版抽样理论与方法（英文版）复分析基础及工程应用（英文版.第3版）机器视觉教程（英文版）（含盘）Java程序设计导论（英文版·第5版）数据挖掘：实用机器学习技术（英文版·第2版）UML参考手册（第2版）UNIX教程（英文版·第2版）软件测试（英文版第2版）设计模式精解（英文版第2版）
目录
Foreword to the first edition
Preface to the second edition
Acknowledgements
1 Propositional logic
1.1 Declarative sentences
1.2 Natural deduction
1.2.1 Rules for natural deduction
1.2.2 Derived rules
1.2.3 Natural deduction in summary
1.2.4 Provable equivalence
1.2.5 An aside: proof by contradiction
1.3 Propositional logic as a formal language
1.4 Semantics of propositional logic
1.4.1 The meaning of logical connectives
1.4.2 Mathematical induction
1.4.3 Soundness of propositional logic
1.4.4 Completeness of propositional logic
1.5 Normal forms
1.5.1 Semantic equivalence, satisfiability and validity
1.5.2 Conjunctive normal forms and validity
1.5.3 Horn clauses and satisfiability
1.6 SAT solvers
1.6.1 A linear solver
1.6.2 A cubic solver
1.7 Exercises
1.8 Bibliographic notes
2 Predicate logic
2.1 The need for a richer language
2.2 Predicate logic as a formal language
2.2.1 Terms
2.2.2 Formulas
2.2.3 Free and bound variables
2.2.4 Substitution
2.3 Proof theory of predicate logic
2.3.1 Natural deduction rules
2.3.2 Quantifier equivalences
2.4 Semantics of predicate logic
214.1 Models
2.4.2 Semantic entailment
2.4.3 The semantics of equality
2.5 Undecidability of predicate logic
2.6 Expressiveness of predicate logic
2.6.1 Existential second-order logic
2.6.2 Universal second-order logic
2.7 Micromodels of software
2.7.1 State machines
2.7.2 Alma - re-visited
2.7.3 A software micromodel
2.8 Exercises
2.9 Bibliographic notes
3 Verification by model checking
3.1 Motivation for verification
3.2 Linear-time temporal logic
3.2.1 Syntax of LTL
3.2.2 Semantics of LTL
3.2.3 Practical patterns of specifications
3.2.4 Important equivalences between LTL formulas
3.2.5 Adequate sets of connectives for LTL
3.3 Model checking: systems, tools, properties
3.3.1 Example: mutual exclusion
3.3.2 The NuSMV model checker
3.3.3 Running NuSMV
3.3.4 Mutual exclusion revisited
3.3.5 The ferryman
3.3.6 The alternating bit protocol
3.4 Branching-time logic
3.4.1 Syntax of CTL
3.4.2 Semantics of CTL
3.4.3 Practical patterns of specifications
3.4.4 Important equivalences between CTL formulas
3.4.5 Adequate sets of CTL connectives
3.5 CTL* and the expressive powers of LTL and CTL
3.5.1 Boolean combinations of temporal formulas in CTL
3.5.2 Past operators in LTL
3.6 Model-checking algorithms
3.6.1 The CTL model-checking algorithm
3.6.2 CTL model checking with fairness
3.6.3 The LTL model-checking algorithm
3.7 The fixed-point characterisation of CTL
3.7.1 Monotone functions
3.7.2 The correctness of SATEG
3.7.3 The correctness of SATEU
3.8 Exercises
3.9 Bibliographic notes
4 Program verification
4.1 Why should we specify and verify code?
4.2 A framework for software verification
4.2.1 A core programming language
4.2.2 Hoare triples
4.2.3 Partial and total correctness
4.2.4 Program variables and logical variables
4.3 Proof calculus for partial correctness
4.3.1 Proof rules
4.3.2 Proof tableaux
4.3.3 A case study: minimal-sum section
4.4 Proof calculus for total correctness
4.5 Programming by contract
4.6 Exercises
4.7 Bibliographic notes Modal logics and agents
5.1 Modes of truth
5.2 Basic modal logic
5.2.1 Syntax
5.2.2 Semantics
5.3 Logic engineering
5.3.1 The stock of valid formulas
5,3.2 Important properties of the accessibility relation
5.3.3 Correspondence theory
5.3.4 Some modal logics
5.4 Natural deduction
5.5 Reasoning about knowledge in a multi-agent system
5.5.1 Some examples
5.5.2 The modal logic KT45n
5.5.3 Natural deduction for KT45n
5.5.4 Formalising the examples
5.6 Exercises
5.7 Bibliographic notes Binary decision diagrams
6.1 Representing boolean functions
6.1.1 Propositional formulas and truth tables
6.1.2 Binary decision diagrams
6.1.3 Ordered BDDs
6.2 Algorithms for reduced OBDDs
6.2.1 The algorithm reduce
6.2.2 The algorithm apply
6.2.3 The algorithm restrict
6.2.4 The algorithm exists
6.2.5 Assessment of OBDDs
6.3 Symbolic model checking
6.3.1 Representing subsets of the set of states
6.3.2 Representing the transition relation
6.3.3 Implementing the functions pre3 and prev
6.3.4 Synthesising OBDDs
6.4 A relational mu-calculus
6.4.1 Syntax and semantics
6.4.2 Coding CTL models and specifications
6.5 Exercises
6.6 Bibliographic notes
Bibliography
Index
</font>
Preface to the second edition
Acknowledgements
1 Propositional logic
1.1 Declarative sentences
1.2 Natural deduction
1.2.1 Rules for natural deduction
1.2.2 Derived rules
1.2.3 Natural deduction in summary
1.2.4 Provable equivalence
1.2.5 An aside: proof by contradiction
1.3 Propositional logic as a formal language
1.4 Semantics of propositional logic
1.4.1 The meaning of logical connectives
1.4.2 Mathematical induction
1.4.3 Soundness of propositional logic
1.4.4 Completeness of propositional logic
1.5 Normal forms
1.5.1 Semantic equivalence, satisfiability and validity
1.5.2 Conjunctive normal forms and validity
1.5.3 Horn clauses and satisfiability
1.6 SAT solvers
1.6.1 A linear solver
1.6.2 A cubic solver
1.7 Exercises
1.8 Bibliographic notes
2 Predicate logic
2.1 The need for a richer language
2.2 Predicate logic as a formal language
2.2.1 Terms
2.2.2 Formulas
2.2.3 Free and bound variables
2.2.4 Substitution
2.3 Proof theory of predicate logic
2.3.1 Natural deduction rules
2.3.2 Quantifier equivalences
2.4 Semantics of predicate logic
214.1 Models
2.4.2 Semantic entailment
2.4.3 The semantics of equality
2.5 Undecidability of predicate logic
2.6 Expressiveness of predicate logic
2.6.1 Existential second-order logic
2.6.2 Universal second-order logic
2.7 Micromodels of software
2.7.1 State machines
2.7.2 Alma - re-visited
2.7.3 A software micromodel
2.8 Exercises
2.9 Bibliographic notes
3 Verification by model checking
3.1 Motivation for verification
3.2 Linear-time temporal logic
3.2.1 Syntax of LTL
3.2.2 Semantics of LTL
3.2.3 Practical patterns of specifications
3.2.4 Important equivalences between LTL formulas
3.2.5 Adequate sets of connectives for LTL
3.3 Model checking: systems, tools, properties
3.3.1 Example: mutual exclusion
3.3.2 The NuSMV model checker
3.3.3 Running NuSMV
3.3.4 Mutual exclusion revisited
3.3.5 The ferryman
3.3.6 The alternating bit protocol
3.4 Branching-time logic
3.4.1 Syntax of CTL
3.4.2 Semantics of CTL
3.4.3 Practical patterns of specifications
3.4.4 Important equivalences between CTL formulas
3.4.5 Adequate sets of CTL connectives
3.5 CTL* and the expressive powers of LTL and CTL
3.5.1 Boolean combinations of temporal formulas in CTL
3.5.2 Past operators in LTL
3.6 Model-checking algorithms
3.6.1 The CTL model-checking algorithm
3.6.2 CTL model checking with fairness
3.6.3 The LTL model-checking algorithm
3.7 The fixed-point characterisation of CTL
3.7.1 Monotone functions
3.7.2 The correctness of SATEG
3.7.3 The correctness of SATEU
3.8 Exercises
3.9 Bibliographic notes
4 Program verification
4.1 Why should we specify and verify code?
4.2 A framework for software verification
4.2.1 A core programming language
4.2.2 Hoare triples
4.2.3 Partial and total correctness
4.2.4 Program variables and logical variables
4.3 Proof calculus for partial correctness
4.3.1 Proof rules
4.3.2 Proof tableaux
4.3.3 A case study: minimal-sum section
4.4 Proof calculus for total correctness
4.5 Programming by contract
4.6 Exercises
4.7 Bibliographic notes Modal logics and agents
5.1 Modes of truth
5.2 Basic modal logic
5.2.1 Syntax
5.2.2 Semantics
5.3 Logic engineering
5.3.1 The stock of valid formulas
5,3.2 Important properties of the accessibility relation
5.3.3 Correspondence theory
5.3.4 Some modal logics
5.4 Natural deduction
5.5 Reasoning about knowledge in a multi-agent system
5.5.1 Some examples
5.5.2 The modal logic KT45n
5.5.3 Natural deduction for KT45n
5.5.4 Formalising the examples
5.6 Exercises
5.7 Bibliographic notes Binary decision diagrams
6.1 Representing boolean functions
6.1.1 Propositional formulas and truth tables
6.1.2 Binary decision diagrams
6.1.3 Ordered BDDs
6.2 Algorithms for reduced OBDDs
6.2.1 The algorithm reduce
6.2.2 The algorithm apply
6.2.3 The algorithm restrict
6.2.4 The algorithm exists
6.2.5 Assessment of OBDDs
6.3 Symbolic model checking
6.3.1 Representing subsets of the set of states
6.3.2 Representing the transition relation
6.3.3 Implementing the functions pre3 and prev
6.3.4 Synthesising OBDDs
6.4 A relational mu-calculus
6.4.1 Syntax and semantics
6.4.2 Coding CTL models and specifications
6.5 Exercises
6.6 Bibliographic notes
Bibliography
Index
</font>
猜您喜欢
