计算世界中的迷人国度

出版时间：1999-12  出版社：东南大学出版社  作者：Wos, Larry; Pieper, Gail W.;  页数：587  

内容概要

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