Background
Moore, J. Strother was born on September 11, 1947 in Seminole, Oklahoma, United States. Son of J. Strother and Jessie Louise Moore.
(This book provides the definitive documentation for one o...)
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 more significant, enduring, and prize-awarded accomplishments in the fields of artificial intelligence, formal methods, and applied logic. The book provides an exact statement of the logic for which the program is a prover, a complete description of the user's commands, installation instructions, and much tutorial information, including references to thousands of pages of examples. Among the examples is a formally verified microprocessor and a formally verified compiler targeting that microprocessor. The second edition of A Computational Logic handbook provides all the information necessry for using the most recently releases version of Nqthm, the freely available"Boyer-Moore"theorem-proving program. The second edition includes a precise description of all recent changes to the logic in the past nine years, including many enhanced syntactic features and rules of inference, which were added to support work on large scale projects in formal methods. Thousands of pages of fascinating, exemplary, mathematically-checked input are described, examples that deal with very difficult questions in formal mehtods and mathematics. New material includes: Description of the new syntax, including COND, CASE, LET, LIST*, and backquote; describes some higher order inference procedures, including"constrained functions"and"functional instantiation"; documents more sophisticated control machinery for manipulating very large theories; introduces a secure proof-checking environment; describes thousands of pages of fascinating example input dealing with very difficult questions in formal methods and mathematics; provides a formal parserfor the syntax; compares the proof complexity of many interesting checked examples; includes much new tutorial help, especially for the many new features. A computational logic is a mathematical logic that is both oriented towards discussion of computation and mechanised so that proofs can be checked by computation. The computational logic discussed in the handbook is that developed by Boyer & Moore. The first edition, published in 1988, is an acknowledged classic in the field of formal methods and computational logic. However it no longer reflects existing technology. The second edition provides a complete overview of the Boyer/Moore theorem proving approach (Nqthm) and provides examples. It includes several significant new features that have been aded to the Nquthm system since 1988. The book is structured in thefollowing way: Part 1 discusses logic without regard for its mechanisation and answers the question what are the axioms and rules of inference? Part 2 discusses its mechanisation and answers the question how does one use the Boyer/Moore theorem prover to prove theorems?
http://www.amazon.com/gp/product/0121229556/?tag=2022091-20
(Computer-Aided Reasoning: An Approach is a textbook intro...)
Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, and theory. It is also appropriate as a reference for business and industry. In this book we present: * A practical functional programming language closely related to Common Lisp; * A formal logic in which defined functions correspond to axioms; * The computer-aided reasoning system ACL2, which includes mechanical support for the proof process. ACL2 is part of the Boyer-Moore family of theorem provers, for which its authors have received the 2005 ACM Software System Award. ACL2 has been successfully applied to projects of commercial interest, including hardware and software verification. Approximately 140 exercises are distributed throughout the book.
http://www.amazon.com/gp/product/B004J8YMAS/?tag=2022091-20
(Computer-Aided Reasoning: An Approach is a textbook intro...)
Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. In this book we present: • A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; • A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; • The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. The ACL2 system has been successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation.
http://www.amazon.com/gp/product/0792377443/?tag=2022091-20
(Contains a precise and complete description of the comput...)
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.
http://www.amazon.com/gp/product/0121229521/?tag=2022091-20
(Computer-Aided Reasoning: An Approach is a textbook intro...)
Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. In this book we present: • A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; • A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; • The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. The ACL2 system has been successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation.
http://www.amazon.com/gp/product/1461370035/?tag=2022091-20
engineer university professor computer scientist
Moore, J. Strother was born on September 11, 1947 in Seminole, Oklahoma, United States. Son of J. Strother and Jessie Louise Moore.
Bachelor of Science in Mathematics, Massachusetts Institute of Technology, 1970. Doctor of Philosophy in Computational Logic, University Edinburgh, Scotland, 1973.
An example of the workings of the Boyer–Moore string search algorithm is given in Moore"s website. Moore received his Bachelor of Science in mathematics at Massachusetts Institute of Technology in 1970 and his Doctor of Philosophy in computational logic at University of Edinburgh in Scotland in 1973. In addition, Moore is a co-author of the ACL2 automated theorem prover.
He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.
Moore was elected to the National Academy of Engineering in 2007, and is a Fellow of the Association for the Advancement of Artificial Intelligence. He is currently the Admiral B.R. Inman Centennial Chair in Computing Theory at The University of Texas at Austin, and was Chair of the Department of Computer Science from 2001-2009. Moore enjoys rock climbing.
(Contains a precise and complete description of the comput...)
(This book provides the definitive documentation for one o...)
(Computer-Aided Reasoning: An Approach is a textbook intro...)
(Computer-Aided Reasoning: An Approach is a textbook intro...)
(Computer-Aided Reasoning: An Approach is a textbook intro...)
Fellow: Association Computing Machinery (Software Systems award 2005), American Association Artificial Intelligence. Member: National Academy of Engineering.
Married Jo Anne O'Neil. Children: Lisa, Jonathan, Chris.