CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

NQTHM: The Boyer-Moore theorem prover.

This directory contains Nqthm-1992, the Boyer-Moore theorem prover. The 1992 version of the theorem prover is upwardly compatible with the previous (1987) version. Included in the distribution are thousands of Nqthm-checked theorems formulated by Bevier, Boyer, Brock, Bronstein, Cowles, Flatau, Hunt, Kaufmann, Kunen, Moore, Nagayama, Russinoff, Shankar, Talcott, Wilding, Yu, and others. The release of Nqthm-1992 includes three revised chapters of the book `A Computational Logic Handbook', including Chapter 4, on the formal logic for which the system is a prover, and Chapter 12, the reference guide to user commands. PC-NQTHM is Matt Kaufmann's interactive proof-checking enhancements to Nqthm-1992.
Origin:  []
   as the file nqthm-1992.tar.Z  []

Version: 1992 (January 1994) Requires: Common Lisp Ports: Nqthm has been tested in AKCL, CMU CL, Allegro CL, Lucid CL, MCL, and Symbolics CL. Copying: Copyright (C) 1989-94 by Robert S. Boyer, J Strother Moore, and Computational Logic, Inc. All Rights Reserved. Use, modification, copying, and distribution permitted, provided you adhere to certain copying policies, as specified in the file basis.lisp. CD-ROM: Prime Time Freeware for AI, Issue 1-1 Mailing List: Send mail to to be added to the mailing list. Author(s): Robert S. Boyer J. Strother Moore Matt Kaufmann Computational Logic Inc. 1717 West 6th Street, Suite 290 Austin, TX 78703-4776 Fax: +1 512-322-0656 Keywords: Authors!Boyer, Authors!Kaufmann, Authors!Moore, Automated Reasoning, Boyer-Moore Theorem Prover, NQTHM, PC-NQTHM, Reasoning!Automated Reasoning, Theorem Proving References: Robert S. Boyer and J. Strother Moore, "A Computational Logic Handbook", Academic Press, 1988. ISBN 0-12-122952-1 ($54.50). (To order a copy, call Academic Press in the USA at 1-800-321-5068, Fax: 1-800-874-6418, or write to Academic Press Books, Customer Service Department, Orlando, FL 32887, USA.)
Last Web update on Mon Feb 13 10:27:34 1995