计算世界中的迷人国度：自动推理导读FASCINATING COUNTRY IN THE WORLD OF COMPUTING, A
点此进入淘宝搜索页搜索分類: 图书,进口原版书,科学与技术 Science & Techology ,
作者： Larry Wos 著
出 版 社： 东南大学出版社
出版时间： 1999-12-1字数：版次： 1页数： 587印刷时间： 2000/03/01开本：印次： 1纸张： 胶版纸I S B N ： 9789810239107包装： 精装内容简介
This book shows you ?through examples and puzzles and intriguing questions ?how to make your computer reason logically. To help you, the book includes a CD-ROM with OTTER, the world's most powerful general-purpose reasoning program. The automation of reasoning has advanced markedly in the past few decades, and this book discusses some of the remarkable successes that automated reasoning programs have had in tackling challenging problems in mathematics, logic, program verification, and circuit design. Because the intended audience includes students and teachers, the book provides many exercises (with hints and also answers), as well as tutorial chapters that gently introduce readers to the field of logic and to automated reasoning in general. For more advanced researchers, the book presents challenging questions, many of which are still unsolved.
目录
Foreword
Preface
Chapter 1 The Menu, The Map, and the Magic
1.1 The Menu for the Grand Feast
1.2 The Book's Audience
1.3 The Map
1.4 Reasoning in Review
1.5 Reasoning by Computer versus Reasoning by a Person . .
1.6 Obstacles to the Effective Automation of Reasoning . . .
1.6.1 Language
1.6.2 Inference Rules
1.6.3 Assignment Completion
1.6.4 StrategT
1.6.5 Redundancy
1.6.6 Specific versus General Information
1.6.7 Conclusion Retention
1.6.8 Conclusion Generation
1.6.9 Inadequate Focus
1.6.10 Conclusion Repetition
1.6.11 Redundancy-Control Transformations
1.6.12 Size of Deduction Step
1.6.13 Metarules for Program Use
1.6.14 Indexing
1.7 Paradigms for Reasoning and for Research
1.8 The Future of Automated Reasoning
Chapter 2 Learning Logic by Example
2.1 and, or, not, if-then (implies)
2.2 A Language for Automated Reasoning Programs
2.2.1 Predicates and Constants
2.2.2 Variables
2.2.3 Functions
2.3 Combinations of or with and, Complex if-then, and
DeMorgan's Laws
2.4 Assumptions and Axioms, Types of Reasoning, and Proof
2.4.1 Assumptions and Axioms
2.4.2 Types of Reasoning, Inference Rules
2.4.3 Proof
2.5 Summary
Chapter 3 Automated Reasoning in Full
3.1 Logic
3.1.1 and
3.1.2 or
3.1.3 not
3.1.4 if-then and implies
3.1.5 is-equivalent-to
3.1.6 Relationships and Laws in Logic
3.2 A Language Understood by an Automated Reasoning Program .
3.2.1 Variables
3.3 Submitting a Problem to a Reasoning Program
3.3.1 Assumptions and Axioms
3.3.2 Special Facts and the Special Hypothesis
3.3.3 Denial of the Goal or Theorem
3.4 Inference Rules
3.4.1 Unification
3.4.2 Binary Resolution
3.4.3 UR-Resolution
3.4.4 Hyperresolution
3.4.5 Paramodulation
3.4.6 Other Inference Rules
3.5 The Empty Clause
3.6 Proof by Contradiction
3.7 Demodulation
3.8 Subsumption
3.9 Strategy
3.9.1 The Set of Support Strategy
3.9.2 Weighting
3.9.3 Unit Preference Strategy
3.9.4 Other Strategies
……
Chapter 4 Logic Circuit Design
Chapter 5 Logic Circuit Validation
Chapter 6 Research in Mathematics
Chapter 7 Research in Formal Logic
Chapter 8 The Formal Treatment of Automated Reasoning
Chapter 9 Wos's Biased Guide for the Effective Use of OTTER
Chapter 10 An Author's Appraisal of His Papers
Chapter 11 Open Questions, Hard Problems, Intriguing Challenges
Chapter 12 Epilogue and After-Dinner Liqueur
Appendix A Featuring Input Files, Proofs, and Output File Fragments
References
Index
