Normal view MARC view ISBD view

Artificial and Mathematical Theory of Computation : Papers in Honor of John Mccarthy.

By: Lifschitz, Vladimir.
Material type: materialTypeLabelBookSeries: eBooks on Demand.Publisher: Saint Louis : Elsevier Science & Technology, 2012Copyright date: ©1991Description: 1 online resource (488 pages).Content type: text Media type: computer Carrier type: online resourceISBN: 9780323148313.Subject(s): Artificial intelligence | Computer programming | Computers | McCarthy, John, -- 1927-2011 | Numerical calculationsGenre/Form: Electronic books.Additional physical formats: Print version:: Artificial and Mathematical Theory of Computation : Papers in Honor of John MccarthyDDC classification: 006.3 Online resources: Click here to view this ebook.
Contents:
Front Cover -- Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy -- Copyright Page -- Tablr of Contents -- Preface -- Contributors List -- Chapter 1. A Short Sketch of the Life and Career of John McCarthy -- Chapter 2. Functional Instantiation in First-Order Logic -- 1 Introduction -- 2 Motivating Example -- 3 Precise Description of the Derived Rules of Inference -- 4 Reference Guide -- 5 Correctness -- 6 Examples -- Acknowledgments -- References -- Chapter 3. Lambda: the Ultimate Combinator -- 1 A-Notation in Programming Logics -- 2 Technical Preliminaries -- 3 Conventional Models -- 4 Homomorphic Models -- 5 Homomorphic Models for the λ-Calculus -- 6 Dynamic Binding -- 7 A Model for the 'λσ-Calculus -- 8 Explicit Sequential Substitutions -- 9 Dynamic Binding Revisited -- 10 Comparison with FP -- 11 History and Related Work -- References -- Chapter 4. Proofs of Termination and the "91" Function -- 1 The "91" Function, Uses and Approaches -- 2 A Well-Foundedness Proof of Terminationof the "91" Function -- 3 Comparison with Some other Proofs -- 4 Principles of Induction on Well-Founded Structures and on FIG Types -- 5 Proofs of Termination and Other Properties of Programs by Induction on FIG Types -- 6 Conclusion -- References -- Chapter 6. Robots with Common Sense? -- References -- Chapter 7. Ascribing Artificial Intelligence to (Simpler) Machines, or When AI Meets the Real World -- 1 Introduction -- 2 SAIL and the FOL Project -- 3 First Commercializations -- 4 Next-Generation Systems -- 5 Discussion -- Acknowledgments -- References -- Chapter 8. The Design of Parallel Programming Languages -- 1 Prelude -- 2 Introduction -- 3 Samefringe -- 4 Design -- 5 Inherited Brands -- 6 Process Environments -- 7 Improved PMI Functions -- 8 Discriminating on Callers -- 9 Waiting for Methods to Be Applicable.
10 Triggered Functions -- 11 Naming Variables Names -- 12 Improved Monotonie Variables -- 13 Temporal or Historical Abstraction -- 14 Correspondences -- 15 Conclusions -- References -- Chapter 9. Metaprogramming at Work in Automated Manufacturing -- 1 Introduction -- 2 The Context -- 3 Outline of the Sil Type System -- 4 Xform -- 5 Designing the Activity of a Single Device -- 6 Designing the Interaction of Devices -- 7 Related Work -- 8 An Appreciation -- References -- Chapter 10.LISP + Calculus = Identities -- 1 Rotational Symmetry -- 2 A Fractal Arc -- 3 The Arc's Fourier Series -- 4 Proof of (1) and (2) -- 5 The Macsyma Function -- 6 Adumbration of (3) -- 7 Nonlocal Derangement -- 8 Proof of (4) and (5) -- References -- Chapter 11. Model Checking vs. Theorem Proving: A Manifesto -- 1 Introduction -- 2 Using the Model-Theoretic Approach -- 3 Discussion and Conclusions -- Acknowledgments -- References -- Chapter 12. Algebraic Computation: The Quiet Revolution -- 1 Introduction -- 2 The Nature of Algebraic Computation -- 3 An Application of Algebraic Computation -- 4 Future Challenges -- 5 Conclusion -- References -- Chapter 13. LISP and Parallelism -- 1 Introduction -- 2 On Parallel Executions of LISP Programs -- 3 PaiLISP -- 4 PaiLISP Implementation Efforts -- Acknowledgments -- References -- Chapter 14. Textbook Examples of Recursion -- 1 The 91 Function -- 2 The Takeuchi Function -- 3 False Takeuchi Functions -- 4 The Takeuchi Recurrence in Higher Dimensions -- Acknowledgments -- References -- Chapter 15. A Metalogic Programming Approach to Multi-Agent Knowledge and Belief -- 1 Introduction -- 2 A logic programming implementation of the provability predicate for propositional Horn clause logic -- 3 Reflection rules -- 4 Extensions of the definition of the demopredicate -- 5 Belief, knowledge, and confidence -- 6 Constants as names of theories.
7 Common knowledge -- 8 The proof -- 9 Conclusion -- Acknowledgement -- References -- Chapter 16. Belief and Introspection -- Foreword -- 1 Introduction -- 2 The System KL -- 3 General Considerations -- 4 Conclusion -- Acknowledgments -- References -- Chapter 17. Monotonicity Properties in Automated Deduction -- Abstract -- 1 Introduction -- 2 Basic Relation-Replacement Rule -- 3 Negative Paramodulation -- 4 Relation Strengthening -- 5 Extended Relation-Replacement Rule -- 6 Completeness -- 7 Relation-Matching Rule -- 8 Computing Matching Formulas -- Acknowledgments -- References -- Chapter 18. Circumscription and Disjunctive Logic Programming -- 1 Introduction -- 2 Preliminaries -- 3 Stratified Disjunctive Logic Programs -- 4 Computing Circumscription -- 5 Conclusion -- Acknowledgments -- References -- Chapter 19. On the Equivalence of Data Representations -- 1 Introduction -- 2 Observable Values and Equivalence -- 3 Function Equivalence -- 4 Typed Lambda Calculus -- 5 Data Representations Determined by the Compiler -- 6 Data-type Declarations -- 7 Data Representations with Free Variables -- Appendix: Typing Rules -- References -- Chapter 20. Caution! Robot Vehicle! -- 1 Introduction -- 2 Cartography -- 3 Fast Cars -- 4 Night Crawlers -- 5 Reflection -- References -- Chapter 21. Circumscription and Authority -- 1 Introduction and Motivation -- 2 Outline of Approach -- 3 Conclusions -- References -- Chapter 22. The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression -- 1 Introduction -- 2 Axiomatizing Change -- 3 A Simple Solution to the Frame Problem (Sometimes) -- 4 Plan Synthesis -- 5 Discussion -- Afterword -- References -- Chapter 23. An Abstraction Mechanism for Symbolic Expressions -- 1 Introduction -- 2 Expressions -- 3 Substitution, Abstraction, and Instantiation.
4 An Example -- References -- Chapter 24. Varieties of Context -- Preface -- 1 Introduction -- 2 Examples of Contexts -- 3 The Structure of Contexts -- 4 Assertions about Contexts -- 5 Semantics for pq -- 6 Final Comments -- Acknowledgements -- References -- Chapter 25. The Influence of the Designeron the Design-J. McCarthyand LISP -- 1 Abstract -- 2 Preparation for the Design -- 3 The First Development of LISP -- 4 The Revision -- 5 Further Concretization -- 6 The Gap -- 7 A Contribution-Nat Rochester -- 8 The First Known Interpreter -- 9 Theoretical Interpreters -- 10 Combining Expressions and Statements -- 11 Garbage Collection -- 12 The Funarg Problem -- 13 The Last Blow -- 14 Conclusion -- References -- Chapter 26. Binding Structures -- 1 Introduction -- 2 Notation Conventions -- 3 Binding Tree Structures -- 4 Binding via Bound Variable Names -- 5 Related Work -- References -- Chapter 27. Logicism, AI, and Common Sense: John McCarthy'sProgram in Philosophical Perspective -- 1 Logicism to Principia Mathematica -- 2 Extensions to the Empirical World -- 3 Linguistic Logicism -- 4 Logicism in AI -- 5 Formalizing Common Sense -- 6 Acknowledgments -- References -- Chapter 28. The Incorrectness of the Bisection Algorithm -- The Proof -- References -- Index.
Summary: Artificial and Mathematical Theory of Computation is a collection of papers that discusses the technical, historical, and philosophical problems related to artificial intelligence and the mathematical theory of computation. Papers cover the logical approach to artificial intelligence; knowledge representation and common sense reasoning; automated deduction; logic programming; nonmonotonic reasoning and circumscription. One paper suggests that the design of parallel programming languages will invariably become more sophisticated as human skill in programming and software developments improves to attain faster running programs. An example of metaprogramming to systems concerns the design and control of operations of factory devices, such as robots and numerically controlled machine tools. Metaprogramming involves two design aspects: that of the activity of a single device and that of the interaction with other devices. One paper cites the application of artificial intelligence pertaining to the project "proof checker for first-order logic" at the Stanford Artificial Intelligence Laboratory. Another paper explains why the bisection algorithm widely used in computer science does not work. This book can prove valuable to engineers and researchers of electrical, computer, and mechanical engineering, as well as, for computer programmers and designers of industrial processes.
Tags from this library: No tags from this library for this title. Log in to add tags.
Item type Current location Call number URL Status Date due Barcode
Electronic Book UT Tyler Online
Online
Q335.5 -- .A77 1991 (Browse shelf) https://ebookcentral.proquest.com/lib/uttyler/detail.action?docID=1129894 Available EBC1129894

Front Cover -- Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy -- Copyright Page -- Tablr of Contents -- Preface -- Contributors List -- Chapter 1. A Short Sketch of the Life and Career of John McCarthy -- Chapter 2. Functional Instantiation in First-Order Logic -- 1 Introduction -- 2 Motivating Example -- 3 Precise Description of the Derived Rules of Inference -- 4 Reference Guide -- 5 Correctness -- 6 Examples -- Acknowledgments -- References -- Chapter 3. Lambda: the Ultimate Combinator -- 1 A-Notation in Programming Logics -- 2 Technical Preliminaries -- 3 Conventional Models -- 4 Homomorphic Models -- 5 Homomorphic Models for the λ-Calculus -- 6 Dynamic Binding -- 7 A Model for the 'λσ-Calculus -- 8 Explicit Sequential Substitutions -- 9 Dynamic Binding Revisited -- 10 Comparison with FP -- 11 History and Related Work -- References -- Chapter 4. Proofs of Termination and the "91" Function -- 1 The "91" Function, Uses and Approaches -- 2 A Well-Foundedness Proof of Terminationof the "91" Function -- 3 Comparison with Some other Proofs -- 4 Principles of Induction on Well-Founded Structures and on FIG Types -- 5 Proofs of Termination and Other Properties of Programs by Induction on FIG Types -- 6 Conclusion -- References -- Chapter 6. Robots with Common Sense? -- References -- Chapter 7. Ascribing Artificial Intelligence to (Simpler) Machines, or When AI Meets the Real World -- 1 Introduction -- 2 SAIL and the FOL Project -- 3 First Commercializations -- 4 Next-Generation Systems -- 5 Discussion -- Acknowledgments -- References -- Chapter 8. The Design of Parallel Programming Languages -- 1 Prelude -- 2 Introduction -- 3 Samefringe -- 4 Design -- 5 Inherited Brands -- 6 Process Environments -- 7 Improved PMI Functions -- 8 Discriminating on Callers -- 9 Waiting for Methods to Be Applicable.

10 Triggered Functions -- 11 Naming Variables Names -- 12 Improved Monotonie Variables -- 13 Temporal or Historical Abstraction -- 14 Correspondences -- 15 Conclusions -- References -- Chapter 9. Metaprogramming at Work in Automated Manufacturing -- 1 Introduction -- 2 The Context -- 3 Outline of the Sil Type System -- 4 Xform -- 5 Designing the Activity of a Single Device -- 6 Designing the Interaction of Devices -- 7 Related Work -- 8 An Appreciation -- References -- Chapter 10.LISP + Calculus = Identities -- 1 Rotational Symmetry -- 2 A Fractal Arc -- 3 The Arc's Fourier Series -- 4 Proof of (1) and (2) -- 5 The Macsyma Function -- 6 Adumbration of (3) -- 7 Nonlocal Derangement -- 8 Proof of (4) and (5) -- References -- Chapter 11. Model Checking vs. Theorem Proving: A Manifesto -- 1 Introduction -- 2 Using the Model-Theoretic Approach -- 3 Discussion and Conclusions -- Acknowledgments -- References -- Chapter 12. Algebraic Computation: The Quiet Revolution -- 1 Introduction -- 2 The Nature of Algebraic Computation -- 3 An Application of Algebraic Computation -- 4 Future Challenges -- 5 Conclusion -- References -- Chapter 13. LISP and Parallelism -- 1 Introduction -- 2 On Parallel Executions of LISP Programs -- 3 PaiLISP -- 4 PaiLISP Implementation Efforts -- Acknowledgments -- References -- Chapter 14. Textbook Examples of Recursion -- 1 The 91 Function -- 2 The Takeuchi Function -- 3 False Takeuchi Functions -- 4 The Takeuchi Recurrence in Higher Dimensions -- Acknowledgments -- References -- Chapter 15. A Metalogic Programming Approach to Multi-Agent Knowledge and Belief -- 1 Introduction -- 2 A logic programming implementation of the provability predicate for propositional Horn clause logic -- 3 Reflection rules -- 4 Extensions of the definition of the demopredicate -- 5 Belief, knowledge, and confidence -- 6 Constants as names of theories.

7 Common knowledge -- 8 The proof -- 9 Conclusion -- Acknowledgement -- References -- Chapter 16. Belief and Introspection -- Foreword -- 1 Introduction -- 2 The System KL -- 3 General Considerations -- 4 Conclusion -- Acknowledgments -- References -- Chapter 17. Monotonicity Properties in Automated Deduction -- Abstract -- 1 Introduction -- 2 Basic Relation-Replacement Rule -- 3 Negative Paramodulation -- 4 Relation Strengthening -- 5 Extended Relation-Replacement Rule -- 6 Completeness -- 7 Relation-Matching Rule -- 8 Computing Matching Formulas -- Acknowledgments -- References -- Chapter 18. Circumscription and Disjunctive Logic Programming -- 1 Introduction -- 2 Preliminaries -- 3 Stratified Disjunctive Logic Programs -- 4 Computing Circumscription -- 5 Conclusion -- Acknowledgments -- References -- Chapter 19. On the Equivalence of Data Representations -- 1 Introduction -- 2 Observable Values and Equivalence -- 3 Function Equivalence -- 4 Typed Lambda Calculus -- 5 Data Representations Determined by the Compiler -- 6 Data-type Declarations -- 7 Data Representations with Free Variables -- Appendix: Typing Rules -- References -- Chapter 20. Caution! Robot Vehicle! -- 1 Introduction -- 2 Cartography -- 3 Fast Cars -- 4 Night Crawlers -- 5 Reflection -- References -- Chapter 21. Circumscription and Authority -- 1 Introduction and Motivation -- 2 Outline of Approach -- 3 Conclusions -- References -- Chapter 22. The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression -- 1 Introduction -- 2 Axiomatizing Change -- 3 A Simple Solution to the Frame Problem (Sometimes) -- 4 Plan Synthesis -- 5 Discussion -- Afterword -- References -- Chapter 23. An Abstraction Mechanism for Symbolic Expressions -- 1 Introduction -- 2 Expressions -- 3 Substitution, Abstraction, and Instantiation.

4 An Example -- References -- Chapter 24. Varieties of Context -- Preface -- 1 Introduction -- 2 Examples of Contexts -- 3 The Structure of Contexts -- 4 Assertions about Contexts -- 5 Semantics for pq -- 6 Final Comments -- Acknowledgements -- References -- Chapter 25. The Influence of the Designeron the Design-J. McCarthyand LISP -- 1 Abstract -- 2 Preparation for the Design -- 3 The First Development of LISP -- 4 The Revision -- 5 Further Concretization -- 6 The Gap -- 7 A Contribution-Nat Rochester -- 8 The First Known Interpreter -- 9 Theoretical Interpreters -- 10 Combining Expressions and Statements -- 11 Garbage Collection -- 12 The Funarg Problem -- 13 The Last Blow -- 14 Conclusion -- References -- Chapter 26. Binding Structures -- 1 Introduction -- 2 Notation Conventions -- 3 Binding Tree Structures -- 4 Binding via Bound Variable Names -- 5 Related Work -- References -- Chapter 27. Logicism, AI, and Common Sense: John McCarthy'sProgram in Philosophical Perspective -- 1 Logicism to Principia Mathematica -- 2 Extensions to the Empirical World -- 3 Linguistic Logicism -- 4 Logicism in AI -- 5 Formalizing Common Sense -- 6 Acknowledgments -- References -- Chapter 28. The Incorrectness of the Bisection Algorithm -- The Proof -- References -- Index.

Artificial and Mathematical Theory of Computation is a collection of papers that discusses the technical, historical, and philosophical problems related to artificial intelligence and the mathematical theory of computation. Papers cover the logical approach to artificial intelligence; knowledge representation and common sense reasoning; automated deduction; logic programming; nonmonotonic reasoning and circumscription. One paper suggests that the design of parallel programming languages will invariably become more sophisticated as human skill in programming and software developments improves to attain faster running programs. An example of metaprogramming to systems concerns the design and control of operations of factory devices, such as robots and numerically controlled machine tools. Metaprogramming involves two design aspects: that of the activity of a single device and that of the interaction with other devices. One paper cites the application of artificial intelligence pertaining to the project "proof checker for first-order logic" at the Stanford Artificial Intelligence Laboratory. Another paper explains why the bisection algorithm widely used in computer science does not work. This book can prove valuable to engineers and researchers of electrical, computer, and mechanical engineering, as well as, for computer programmers and designers of industrial processes.

Description based on publisher supplied metadata and other sources.

There are no comments for this item.

Log in to your account to post a comment.