The Automation of Reasoning

The Automation of Reasoning : An Experimenter's Notebook with Otter Tutorial

By (author) 

List price: US$117.00

Currently unavailable

Add to wishlist

AbeBooks may have this title (opens in new window).

Try AbeBooks


This landmark title is the only one of its kind to offer research problems in the field along with guidance in using and implementing what has been called the most powerful general-purpose program for automated reasoning available: Bill McCune's OTTER. The remarkable automated reasoning program is included (on diskette) with the text to allow hands-on understanding of the author's imparted knowledge. Also included within the text are detailed guidelines for using the program, which can be of great assistance in deductive reasoning. The text covers, in depth, how research is actually conducted using an automated reasoning program and based on the author's thirty years of work in the field, and also offers new results in mathematics and in logic that have never before appeared in print.
show more

Product details

  • Hardback | 434 pages
  • 158.2 x 234.4 x 27.9mm | 920.65g
  • Academic Press Inc
  • San Diego, United States
  • English
  • 0127634207
  • 9780127634203

Table of contents

(Chapter Headings): A Sterling Pursuit. Scott's Challenge. Provocative Obstacles and the Means for Quashing Them. The Methodology by Example. Lukasiewicz's Challenge. Group Theory. Robbins Algebra. A Biased Guide for Choosing OTTER Options. Seeking Proofs Satisfying a Given Property. Proof Checking. Experimental Potpourri. Research Topics. Additional Useful Notes. A Demanding and Noble Endeavor. Appendices. Subject Index.
show more

About Larry Wos

Larry Wos received his Ph.D. in Mathematics from the University of Illinois. He is now Senior Mathematician in the Mathematics and Computer Science division of Argonne National Laboratory, where he has worked for more than 30 years. Other books by the author include Automated Reasoning: Introduction and Applications and Automated Reasoning: 33 Basic Research Problems.
show more