Automated Theorem Proving : Theory and Practice

Monty Newborn

ISBN 10: 0387950753 / ISBN 13: 9780387950754

Published by Springer New York Dez 2000, 2000

About this Item

Neuware - As the 21st century begins, the power of our magical new tool and partner, the computer, is increasing at an astonishing rate. Computers that perform billions of operations per second are now commonplace. Multiprocessors with thousands of little computers - relatively little! -can now carry out parallel computations and solve problems in seconds that only a few years ago took days or months. Chess-playing programs are on an even footing with the world's best players. IBM's Deep Blue defeated world champion Garry Kasparov in a match several years ago. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from given facts, or abstractly, to prove theorems-the subject of this book. Specifically, this book is about two theorem-proving programs, THEO and HERBY. The first four chapters contain introductory material about automated theorem proving and the two programs. This includes material on the language used to express theorems, predicate calculus, and the rules of inference. This also includes a description of a third program included with this package, called COMPILE. As described in Chapter 3, COMPILE transforms predicate calculus expressions into clause form as required by HERBY and THEO. Chapter 5 presents the theoretical foundations of seman tic tree theorem proving as performed by HERBY. Chapter 6 presents the theoretical foundations of resolution-refutation theorem proving as per formed by THEO. Chapters 7 and 8 describe HERBY and how to use it.

Seller Inventory # 9780387950754

Bibliographic Details

• Title: Automated Theorem Proving : Theory and Practice
• Publisher: Springer New York Dez 2000
• Publication Date: 2000
• Language: English
• ISBN 10: 0387950753
• ISBN 13: 9780387950754
• Binding: Buch
• Condition: Neu

About this title

Synopsis

As the 21st century begins, the power of our magical new tool and partner, the computer, is increasing at an astonishing rate. Computers that perform billions of operations per second are now commonplace. Multiprocessors with thousands of little computers - relatively little! -can now carry out parallel computations and solve problems in seconds that only a few years ago took days or months. Chess-playing programs are on an even footing with the world's best players. IBM's Deep Blue defeated world champion Garry Kasparov in a match several years ago. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from given facts, or abstractly, to prove theorems-the subject of this book. Specifically, this book is about two theorem-proving programs, THEO and HERBY. The first four chapters contain introductory material about automated theorem proving and the two programs. This includes material on the language used to express theorems, predicate calculus, and the rules of inference. This also includes a description of a third program included with this package, called COMPILE. As described in Chapter 3, COMPILE transforms predicate calculus expressions into clause form as required by HERBY and THEO. Chapter 5 presents the theoretical foundations of seman­ tic tree theorem proving as performed by HERBY. Chapter 6 presents the theoretical foundations of resolution-refutation theorem proving as per­ formed by THEO. Chapters 7 and 8 describe HERBY and how to use it.

Synopsis

This text and software package introduces the reader to automated theorem proving and provides two approaches implemented as easy-to-use programs. The two approaches studied are semantic tree theorem proving and resolution-refutation theorem proving. The first chapters introduce the reader to first-order predicate calculus, well-formed formulae, and their transformation to clauses (implemented in a third program provided on diskette). Then the author shows how the two methods work and provides numerous examples for readers to try their hand at theorem-proving experiments. Each chapter comes with exercises intended to familiarise the readers with the ideas and with the software, and answers are provided to many of the problems.