rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    non sort: A
    title: computational logic
  name:
    name part: Boyer, Robert S.
    role:
      role term: creator
  name:
    name part: Moore, J Strother
    name part: 1947-
    role:
      role term: author.
  name:
    name part: ScienceDirect (Online service)
  type of resource: text
  genre: bibliography
  genre: Electronic books.
  origin info:
    place:
      place term: nyu
    date issued: 1979
    issuance: monographic
  language:
    language term: eng
  physical description:
    reformatting quality: access
    form: remote
    extent: 1 online resource (xiv, 397 pages)
  table of contents: 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
  table of contents: 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
  table of contents: 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
  table of contents: 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
  table of contents: 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
  note: Robert S. Boyer and J Strother Moore.
  note: 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
  note: digitized 2010 HathiTrust Digital Library committed to preserve pda MiAaHDL
  note: Includes bibliographical references (pages 385-387) and index.
  note: English.
  subject:
    topic: Automatic theorem proving
  subject:
    topic: Théorèmes
    topic: Démonstration automatique
  subject:
    topic: MATHEMATICS
    topic: General
  subject:
    topic: Automatic theorem proving
  subject:
    topic: Automatisches Beweisverfahren
  subject:
    topic: MATHEMATICAL LOGIC
  subject:
    topic: THEOREM PROVING
  subject:
    topic: Automatic theorem proving
  subject:
    topic: Logic, Symbolic and mathematical
  subject:
    topic: Logique informatique
  classification: QA76.9.A96 B68 1979eb
  classification: 519.4
  classification: 001.53/5
  classification: 31.10
  classification: ES 215
  classification: ST 140
  related item:
    title info:
      title: Computational logic
    name:
      name part: Boyer, Robert S.
    origin info:
      publisher: New York : Academic Press, ©1979
    identifier: (DLC) 79051693
    identifier: (OCoLC)5196669
  related item:
    identifier: (DLC) 79051693
    identifier: (OCoLC)5196669
  related item:
    title info:
      title: ACM monograph series
  identifier: 9780121229504
  identifier: 0121229505
  identifier: 9781483277882
  identifier: 1483277887
  identifier: 9781322470108
  identifier: 1322470103
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: OCLCE
    record creation date: 100325
    record change date: 20260326172921.7
    record identifier: in00005740843
    language of cataloging:
      language term: eng