Nqthm

A 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).