計算世界中的迷人國度

內(nèi)容概要

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.

書籍目錄

ForewordPrefaceChapter 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 ReasoningChapter 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  SummaryChapter 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 DesignChapter 5 Logic Circuit ValidationChapter 6 Research in MathematicsChapter 7 Research in Formal LogicChapter 8 The Formal Treatment of Automated ReasoningChapter 9 Wos's Biased Guide for the Effective Use of OTTERChapter 10 An Author's Appraisal of His PapersChapter 11 Open Questions, Hard Problems, Intriguing ChallengesChapter 12 Epilogue and After-Dinner LiqueurAppendix A Featuring Input Files, Proofs, and Output File FragmentsReferencesIndex

圖書封面

評論、評分、閱讀與下載

---

    計算世界中的迷人國度 PDF格式下載

---