Research Catalog
The automation of reasoning : an experimenter's notebook with OTTER tutorial
- Title
- The automation of reasoning : an experimenter's notebook with OTTER tutorial / Larry Wos.
- Author
- Wos, Larry.
- Publication
- San Diego : Academic Press, [1996], ©1996.
Items in the Library & Off-site
Filter by
1 Item
| Status | Vol/Date | Format | Access | Call Number | Item Location |
|---|---|---|---|---|---|
Not available - Please for assistance. | book & computer diskette | Text | Request in advance | QA76.9.A96 W68 1996 book & computer diskette | Off-site |
Holdings
Details
- Description
- xiv, 434 pages; 24 cm +
- Summary
- This book presents some of the insights, judgements, opinions, and experiences gleaned from more than 30 years of research in automated reasoning. The style and organization are those of an experimenter's notebook, featuring both successes and failures resulting from numerous experiments with one of the world's most powerful software packages for automated reasoning, Bill McCune's OTTER.
- Subject
- Automatic theorem proving
- Bibliography (note)
- Includes bibliographical references (p. 419-421) and index.
- Contents
- 1. A Sterling Pursuit -- 2. Scott's Challenge -- 3. Provocative Obstacles and the Means for Quashing Them -- 4. The Methodology by Example -- 5. Lukasiewicz's Challenge -- 6. Group Theory -- 7. Robbins Algebra -- 8. A Biased Guide for Choosing OTTER Options -- 9. Seeking Proofs Satisfying a Given Property -- 10. Proof Checking -- 11. Experimental Potpourri -- 12. Research Topics -- 13. Additional Useful Notes -- 14. A Demanding and Noble Endeavor -- Appendix A. Featuring Various Strategies -- Appendix B. Example I Files and Proofs and Input File for Cursory Proof Checking -- Appendix C. Example 2 Files and Proofs and Files for Rigorous Proof Checking.
- ISBN
- 0127634207 (alk. paper)
- LCCN
- 96022986
- OCLC
- ocm34839715
- Owning Institutions
- Columbia University Libraries