CMU Artificial Intelligence Repository
NQTHM: The Boyer-Moore theorem prover.
areas/reasonng/atp/systems/nqthm/
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:
ftp.cli.com:/pub/nqthm/nqthm-1992/ [192.31.85.129]
as the file nqthm-1992.tar.Z
ftp.cli.com:/pub/pc-nqthm/pc-nqthm-1992/ [192.31.85.129]
pc-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 nqthm-users-request@cli.com 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
AI.Repository@cs.cmu.edu