Nqthm


Also found in: Wikipedia.

Nqthm

The language used in the Boyer-Moore theorem prover.

["Proving Theorems About LISP Functions", R.S. Boyer et al JACM 22(1):129-144 (Jan 1975)].
References in periodicals archive ?
Moore discussed the capabilities of the ACL2 system (the successor of the Boyer-Moore NQTHM prover).
In fact, the Nqthm theorem prover [Boyer and Moore 1988] uses type information internally, even though the logic is untyped.
For recent notable work, I focus on some significant theorem-proving systems: the geometry theorem provers of Chou (Chou, Gao, and Zhang 1994; Chou 1988); the Boyer and Moore (1988) interactive theorem prover NQTHM and its successor ACL2 (Kaufmann and Moore 1996); the rewrite rule laboratory (RRL) of Kaput and Zhang (1995); the resolution prover OTTER (McCune and Otter 1997; McCune 1994) and the equational logic prover EQP by McCune (1996); the interactive higher-order logic provers NUPRL (Constable et al.
The ACL2 prover (Kaufmann and Moore 1996), the successor of NQTHM, recently was used interactively to obtain a formal proof of the correctness of the floating-point divide code for AMD's newest PENTIUM-like microprocessor.
The ability to tackle these real-world problems is primarily the result of the improved capabilities of interactive systems such as NQTHM, ACL2, PVS, NUPRL, HOL, COQ (Coquand and Huet [INRIA] 1988), and ISABELLE (Paulson [Cambridge] 1994).
However, many other systems now have user communities of their own, some sizable: NQTHM, ACL2, and RRL, for example, and the higher-order logic systems HOL, NUPRL, ISABELLE, PVS, COQ, and TPS.
Some systems that are partially successful in combining techniques are PVS, NQTHM, ACL2, HOL, EVES (Craigen et al.