http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
Front Cover; A Computational Logic; Copyright Page; Dedication; Table of Contents; Preface; Chapter 1. Introduction; A. Motivation; B. Our Formal Theory; C. Proof Techniques; D. Examples; E. Our Mechanical Theorem-Prover; F. Artificial Intelligence or Logic?; G. Organization; Chapter 2. A Sketch of the Theory and Two Simple Examples; A. An Informal Sketch of the Theory; B.A Simple Inductive Proof; C.A More Difficult Problem; D.A More Difficult Proof; E. Summary; F. Notes; Chapter 3. A Precise Definition of the Theory; A. Syntax; B. The Theory of IF and EQUAL; C. Well-Founded Relations
D. InductionE. Shells; F. Natural Numbers; G. Literal Atoms; H. Ordered Pairs; I. Definitions; J. Lexicographic Relations; K. LESSP and COUNT; L. Conclusion; Chapter 4. The Correctness of a Tautology-Checker; A. Informal Development; B. Formal Specification of the Problem; C. The Former Definition of TAUTOLOGY. CHECKER; D. The Mechanical Proofs; E. Summary; F. Notes; Chapter 5. An Overview of How We Prove Theorems; A. The Role of the User; B. Clausal Representation of Conjectures; C. The Organization of Our Heuristics; D. The Organization of Our Presentation
Chapter 6. Using Type Information to Simplify FormulasA. Type Sets; B. Assuming Expressions True or False; C. Computing Type Sets; D. Type Prescriptions; E. Summary; F. Notes; Chapter 7. Using Axioms and Lemmas as Rewrite Rules; A. Directed Equalities; B. Infinite Looping; C. More General Rewrite Rules; D. An Example of Using Rewrite Rules; E. Infinite Backwards Chaining; F. Free Variables in Hypotheses; Chapter 8. Using Definitions; A. Nonrecursive Functions; B. Computing Values; C. Diving in to See; Chapter 9. Rewriting Terms and Simplifying Clauses; A. Rewriting Terms
B. Simplifying ClausesC. The REVERSE Example; D. Simplification in the REVERSE Example; Chapter 10. Eliminating Destructors; A. Trading Bad Terms for Good Terms; B. The Form of Elimination Lemmas; C. The Precise Use of Elimination Lemmas; D.A Nontrivial Example; E. Multiple Destructors and Infinite Looping; F. When Elimination Is Risky; G. Destructor Elimination in the REVERSE Example; Chapter 11. Using Equalities; A. Using and Throwing Away Equalities; B. Cross-Fertilization; C.A Simple Example of Cross-Fertilization; D. The Precise Use of Equalities
E. Cross-Fertilization in the REVERSE ExampleChapter 12. Generalization; A.A Simple Generalization Heuristic; B. Restricting Generalizations; C. Examples of Generalizations; D. The Precise Statement of the Generalization Heuristic; E. Generalization in the REVERSE Example; Chapter 13. Eliminating Irrelevance; A. Two Simple Checks for Irrelevance; B. The Reason for Eliminating Isolated Hypotheses; C. Elimination of Irrelevance in the REVERSE Example; Chapter 14. Induction and the Analysis of Recursive Definitions; A. Satisfying the Principle of Definition
Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002. http://purl.oclc.org/DLF/benchrepro0212 MiAaHDL
digitized 2010 HathiTrust Digital Library committed to preserve pda MiAaHDL
Includes bibliographical references (pages 385-387) and index.