| 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 |
内容加载中，请稍后...
商品评论（0条）