Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning
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.
1136609962
Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning
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.
146.0 Out Of Stock
Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning

Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning

by Gail W Pieper, Larry Wos
Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning

Fascinating Country In The World Of Computing, A: Your Guide To Automated Reasoning

by Gail W Pieper, Larry Wos

Hardcover(BK&CD ROM)

$146.00 
  • SHIP THIS ITEM
    Temporarily Out of Stock Online
  • PICK UP IN STORE

    Your local store may have stock of this item.

Related collections and offers


Overview

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.

Product Details

ISBN-13: 9789810239107
Publisher: World Scientific Publishing Company, Incorporated
Publication date: 12/02/1999
Edition description: BK&CD ROM
Pages: 608
Product dimensions: 6.50(w) x 8.80(h) x 1.50(d)

Table of Contents

Forewordvii
Prefaceix
Chapter 1The Menu, The Map, and the Magic1
1.1The Menu for the Grand Feast3
1.2The Book's Audience5
1.3The Map7
1.4Reasoning in Review8
1.5Reasoning by Computer versus Reasoning by a Person10
1.6Obstacles to the Effective Automation of Reasoning13
1.6.1Language14
1.6.2Inference Rules15
1.6.3Assignment Completion16
1.6.4Strategy17
1.6.5Redundancy17
1.6.6Specific versus General Information18
1.6.7Conclusion Retention18
1.6.8Conclusion Generation19
1.6.9Inadequate Focus20
1.6.10Conclusion Repetition21
1.6.11Redundancy-Control Transformations22
1.6.12Size of Deduction Step22
1.6.13Metarules for Program Use23
1.6.14Indexing23
1.7Paradigms for Reasoning and for Research23
1.8The Future of Automated Reasoning26
Chapter 2Learning Logic by Example29
2.1and, or, not, if-then (implies)29
2.2A Language for Automated Reasoning Programs35
2.2.1Predicates and Constants36
2.2.2Variables37
2.2.3Functions39
2.3Combinations of or with and, Complex if-then, and DeMorgan's Laws44
2.4Assumptions and Axioms, Types of Reasoning, and Proof45
2.4.1Assumptions and Axioms46
2.4.2Types of Reasoning, Inference Rules47
2.4.3Proof50
2.5Summary56
Chapter 3Automated Reasoning in Full63
3.1Logic64
3.1.1and64
3.1.2or64
3.1.3not65
3.1.4if-then and implies65
3.1.5is-equivalent-to65
3.1.6Relationships and Laws in Logic65
3.2A Language Understood by an Automated Reasoning Program67
3.2.1Variables68
3.3Submitting a Problem to a Reasoning Program70
3.3.1Assumptions and Axioms70
3.3.2Special Facts and the Special Hypothesis70
3.3.3Denial of the Goal or Theorem71
3.4Inference Rules72
3.4.1Unification72
3.4.2Binary Resolution73
3.4.3UR-Resolution74
3.4.4Hyperresolution75
3.4.5Paramodulation76
3.4.6Other Inference Rules78
3.5The Empty Clause79
3.6Proof by Contradiction79
3.7Demodulation80
3.8Subsumption82
3.9Strategy84
3.9.1The Set of Support Strategy84
3.9.2Weighting85
3.9.3Unit Preference Strategy85
3.9.4Other Strategies86
3.10An Automated Reasoning Program in Action87
3.11Otter and Earlier Automated Theorem-Proving Programs89
3.11.1The Basic Argonne Paradigm93
3.11.2A Sequential Theorem-Proving Algorithm94
3.11.3Implementing the Algorithm on Shared-Memory Multiprocessors95
3.11.4Implementing the Algorithm on Distributed-Memory Machines98
3.12Answers to Exercises100
Chapter 4Logic Circuit Design107
4.1Introduction to Logic Circuit Design107
4.1.1Components of Logic Circuits108
4.1.1.1And, or, and not gates108
4.1.1.2Other Basic Components109
4.1.2Specifications110
4.1.3Problems for the Circuit Designer111
4.2Circuit Design Using Demodulation112
4.2.1Designing from Functional Specifications112
4.2.2Designing from Descriptive Sentences116
4.2.3Designing from Tables117
4.2.4Advantages and Disadvantages of the Demodulation Approach119
4.3Circuit Design Using Hyperresolution119
4.3.1The Output Predicate120
4.3.2Construction Rules120
4.3.3Examples121
4.3.4Achievable Signals and the Output Predicate124
4.4Solution to the Two-Inverter Puzzle124
4.4.1Some New Complexities125
4.4.2The First Formulation126
4.4.3Reversions131
4.4.4Solving the Puzzle Faster134
4.5Multivalued Logic Design Using Negative Hyperresolution137
4.5.1T-gates138
4.5.2Representation of Multivalued Logic Functions138
4.5.3Construction Rules139
4.5.4Negative Hyperresolution139
4.5.5An Example140
4.6Answers to Exercises142
Chapter 5Logic Circuit Validation147
5.1What Is Validation?147
5.2Simple Example148
5.3Important Features of the Example150
5.3.1Validation as Language Translation150
5.3.2Canonicalization151
5.3.3Simplification152
5.3.4Commutativity-Type Demodulators and Lexical Ordering152
5.4A More Complex Example153
5.5Validating an Adder157
5.5.1The One-Bit Full Adder157
5.5.2Combining Validated Subcircuits161
5.6Answers to Exercises163
Chapter 6Research in Mathematics165
6.1A Simple Example166
6.2A Simple Example Revisited171
6.2.1The Set of Support Strategy and the Simple Example174
6.2.2Weighting Applied to the Example178
6.2.3Demodulation, Canonicalization, and Simplification180
6.2.4Subsumption and Redundancy182
6.3Answering Open Questions187
6.4Model and Counterexample Generation190
6.5Representable Concepts: Easy and Difficult197
6.6Review199
6.7Using Otter to Find Shorter Proofs200
6.8Answers to Exercises205
Chapter 7Research in Formal Logic211
7.1Equivalential Calculus212
7.2A Simple Example213
7.3Imposing Knowledge and Intuition215
7.4Answering Open Questions in Equivalential Calculus217
7.4.1Finding Useful Notation219
7.4.2Suggesting Conjectures220
7.5Propositional Calculus221
7.5.1Proof by Analogy and Other Techniques for Solving Hard Problems222
7.5.2Seeking Shorter Proofs224
7.5.3Finding New Axiom Systems228
7.6Combinatory Logic230
7.6.1Constructing Objects231
7.6.2Successes in Combinatory Logic233
7.7Using Otter to Seek Shorter Proofs in Two-Valued Sentential Calculus234
7.8Using Otter to Construct Combinations242
7.9Answers to Exercises248
Chapter 8The Formal Treatment of Automated Reasoning255
8.1First-Order Predicate Calculus255
8.1.1The Language of Fopc256
8.1.2The Semantics of Fopc260
8.1.3The Calculus of Fopc and the Concept of Proof262
8.2The Clause Language265
8.3Inference Rules270
8.3.1Binary Resolution274
8.3.2Refutation Completeness278
8.4Strategy285
8.5Other Inference Rules291
8.6Subsumption298
8.7Demodulation299
8.8Answers to Exercises301
Chapter 9Wos's Biased Guide for the Effective Use of Otter309
9.1Overview to Option Selection312
9.2Option Choosing313
9.2.1Representation313
9.2.2Strategy315
9.2.2.1Set of Support Strategy315
9.2.2.2Weighting317
9.2.2.3Level Saturation320
9.2.2.4Ratio Strategy321
9.2.2.5Tail Strategy and Recursive Tail Strategy322
9.2.2.6Resonance Strategy and Resonance-Restriction Strategy324
9.2.2.7Subtautology326
9.2.3Hot List Strategy and Dynamic Hot List Strategy326
9.2.4Inference Rules327
9.2.4.1UR-Resolution327
9.2.4.2Hyperresolution328
9.2.4.3Paramodulation329
9.2.4.4Hyperparamodulation330
9.2.4.5Binary Resolution330
9.2.5Subsumption, for Purging Redundant Information330
9.2.6Demodulation, for Simplification and Canonicalization332
9.2.7List Usage334
9.3An Emphasis on Experimentation338
9.4Four Useful Input Files339
9.4.1A Puzzle to Solve339
9.4.2A Theorem to Prove342
9.4.3A Shorter Proof to Find343
Chapter 10An Author's Appraisal of His Papers347
10.1On Commutative Prime Power Subgroups of the Norm349
10.2The Unit Preference Strategy in Theorem Proving351
10.3Efficiency and Completeness of the Set of Support Strategy in Theorem Proving355
10.4Automatic Generation of Proofs in Mathematics364
10.5The Concept of Demodulation in Theorem Proving366
10.6Paramodulation and Set of Support371
10.7Axiom Systems in Automatic Theorem Proving375
10.8Paramodulation and Theorem-Proving in First-Order Theories with Equality377
10.9Maximal Models and Refutation Completeness386
10.10A Theorem-Proving Language for Experimentation388
10.11Unit Refutations and Horn Sets388
10.12Problems and Experiments for and with Automated Theorem-Proving Programs389
10.13Complexity and Related Enhancements for Automated Theorem-Proving Programs391
10.14Unnatural Attack on the Structure Problem for the Free Jordan Ring on 3 Letters395
10.15Automated Generation of Models and Counterexamples396
10.16Hyperparamodulation: A Refinement of Paramodulation399
10.17Semigroups, Antiautomorphisms, and Involutions402
10.18An Automated Reasoning System404
10.19Solving Open Questions with an Automated Theorem-Proving Program405
10.20Demodulation and Related Tricks406
10.21Automated Theorem-Proving 1965-1970408
10.22Shortest Single Axioms in Equivalential Calculus408
10.23Automated Reasoning: Real Uses and Potential Uses411
10.24Equivalential Calculus and Infinite Domains412
10.25Open Questions Solved with the Assistance of Aura413
10.26The Linked Inference Principle, II: The User's Viewpoint414
10.27Achievements in Automated Reasoning417
10.28Automated Reasoning Programs: How They Work417
10.29Automated Reasoning418
10.30What Is Automated Reasoning?419
10.31Automating Reasoning419
10.32Job-Shop Scheduling Using Automated Reasoning420
10.33Negative Paramodulation421
10.34Set Theory in First-Order Logic: Clauses for Godel's Axioms423
10.35Resolution, Binary425
10.36Finding Sages in Combinatory Logic426
10.37Challenge Problems Focusing on Equality and Combinatory Logic428
10.38Automated Theorem Proving and Logic Programming: A Natural Symbiosis431
10.39Subsumption, A Sometimes Undervalued Procedure432
10.40Applications of Automated Reasoning433
10.41Meeting the Challenge of Fifty Years of Logic434
10.42The Absence and the Presence of Fixed Point Combinators437
10.43Automated Reasoning Contributes to Mathematics and Logic438
10.44Automated Reasoning and Bledsoe's Dream for the Field439
10.45A Logical Basis for the Automation of Reasoning: Case Studies440
10.46The Linked Inference Principle, I: The Formal Treatment441
10.47The Application of Automated Reasoning to Questions in Mathematics and Logic443
10.48Automated Reasoning and Enumerative Search443
10.49Benchmark Problems in Which Equality Plays the Major Role444
10.50Automated Deduction with Condensed Detachment445
10.51Single Axioms for Exponent Groups447
10.52The Impossibility of the Automation of Logical Reasoning449
10.53The Kernel Strategy and Its Use for the Study of Combinatory Logic450
10.54Automated Reasoning Answers Open Questions453
10.55The Field of Automated Reasoning456
10.56The Resonance Strategy456
10.57Searching for Circles of Pure Proofs461
10.58The Power of Combining Resonance with Heat463
10.59The Hot List Strategy466
10.60Otter and the Moufang Identity Problem471
10.61Automating the Search for Elegant Proofs472
10.62Otter: The Cade-13 Competition Incarnations478
10.63Programs That Offer Fast, Flawless, Logical Reasoning480
10.64Hints and Answers480
10.64.1Hints
From the B&N Reads Blog

Customer Reviews