راهنمای منطق محاسباتی: پیشینۀ یادداشت‌ها و گزارش‌ها در علوم کامپیوتر و ریاضیات کاربردی

This book is a user's guide to a computational logic. A "computational logic" is a mathematical logic that is both oriented towards discussion of computation and mechanized so that proofs can be checked by computation. The computational logic discussed in this handbook is that developed by Boyer and Moore. This handbook contains a precise and complete description of our logic and a detailed reference guide to the associated mechanical theorem proving system. In addition, the handbook includes a primer for the logic as a functional programming language, an introduction to proofs in the logic, a primer for the mechanical theorem prover, stylistic advice on how to use the logic and theorem prover effectively, and many examples. The logic was last described completely in our book A Computational Logic, [4], published in 1979. The main purpose of the book was to describe in detail how the theorem prover worked, its organization, proof techniques, heuristics, etc. One measure of the success of the book is that we know of three independent successful efforts to construct the theorem prover from the book. Perspectives in Computing: A Computational Logic Handbook contains a precise description of the logic and a detailed reference guide to the associated mechanical theorem proving system, including a primer for the logic as a functional programming language, an introduction to proofs in the logic, and a primer for the mechanical theorem. The publication first offers information on a primer for the logic, formalization within the logic, and a precise description of the logic. Discussions focus on induction and recursion, quantification, explicit value terms, dealing with features and omissions, elementary mathematical relationships, Boolean operators, and conventional data structures. The text then takes a look at proving theorems in the logic, mechanized proofs in the logic, and an introduction to the system. The text examines the processes involved in using the theorem prover, four classes of rules generated from lemmas, and aborting or interrupting commands. Topics include executable counterparts, toggle, elimination of irrelevancy, heuristic use of equalities, representation of formulas, type sets, and the crucial check points in a proof attempt. The publication is a vital reference for researchers interested in computational logic. Content: Inside Front Cover, Page ii Front Matter, Page iii Copyright, Page iv Preface, Pages xi-xvi 1 - Introduction, Pages 3-13 2 - A Primer for the Logic, Pages 15-56 3 - Formalization Within the Logic, Pages 57-92 4 - A Precise Description of the Logic, Pages 93-141 5 - Proving Theorems in the Logic, Pages 143-164 6 - Mechanized Proofs in the Logic, Pages 167-175 7 - An Introduction to the System, Pages 177-185 8 - A Sample Session with the Theorem Prover, Pages 187-205 9 - How to Use the Theorem Prover, Pages 207-217 10 - How the Theorem Prover Works, Pages 219-229 11 - The Four Classes of Rules Generated from Lemmas, Pages 231-249 12 - Reference Guide, Pages 251-313 13 - Hints on Using the Theorem Prover, Pages 315-334 14 - Installation Guide, Pages 335-349 Appendix I - A Parser for the Syntax, Pages 351-382 Appendix II - The Primitive Shell Axioms, Pages 383-390 Appendix III - On the Difficulty of Proofs, Pages 391-395 References, Pages 397-399 Index, Pages 401-408 Perspectives in Computing, Pages ibc1-ibc2

this Book Provides The Definitive Documentation For One Of The Most Well-known And Highly Regarded Theorem-proving Programs Ever Written. The Program Described Is One Of The ...

booknews

contains A Precise And Complete Description Of The Computational Logic Developed By The Authors; Will Serve Also As A Reference Guide To The Associated Mechanical Theorem Proving System. Annotation C. Book News, Inc., Portland, Or (booknews.com)

Contains a precise and complete description of the computational logic develo by the authors; will serve also as a reference guide to the associated mechanical theorem proving system. Annotation copyright Book News, Inc. Portland, Or.