Talk:Nqthm

I started this article, as I spent 7 years of my life (i.e. my dissertation work) using this prover. If there are any questions or additions needed, please contact me on my German talk page (never read my english one): http://de.wikipedia.org/wiki/Benutzer_Diskussion:WiseWoman . English is fine. --WiseWoman 07:54, 8 January 2007 (UTC)

Name

Anyone know where the name comes from? "thm" may stand for theorem, but what about "Nq"? --MarSch 22:10, 27 October 2007 (UTC)

Yes -- the `Nq' stand for `Non-quantified.' `Nqthm' was originally the directory name for the path of their (nameless) quantifier free prover. Eventually the directory name stuck as the name of the prover itself. —Preceding unsigned comment added by 66.68.108.112 (talk) 07:14, 2 January 2008 (UTC)

Example proof of multiplication commutativity

• The proof should have an own section. Currently, it seems to start in section "Definitions" (at "This is an example of the proof ..."), and to countinue in section "Theorem formulation".
• The prover output seems to be cut-off too early, as after the sentence "the following two new conjectures" only one conjecture is shown, viz. "Case 2". Maybe "Case 1" should be moved from the start of the following output box to the end of this one?
• In order to get an impression of how the prover works, I'd like to see the whole proof somewhere. As far as I know, a proof of the commutativity of "*" needs as lemmas commutativity and associativity of "+" and the original as well as the mirrored recursive definitions of "*" and "+" (that is, e.g. "x+0=x" as well as "0+x=x", only one of which is usually a definition). Are they all supposed to be readily available in the knowledge basis of the system before the shown proof is attempted? Else, could some of them be conjectured automatically during the proof process? Could the "cross-fertilization" (wasn't that term coined by Boyer+Moore? - it should be explained somewhere on wikipedia) technique be used for conjecturing?
• In the "Definitions" section, I didn't understand what "ground-zero", "bootstrapping", and "satellite" should mean.

Jochen Burghardt (talk) 19:36, 23 May 2013 (UTC)

Lisp

The article suggests that the system was implemented on top of Common Lisp, but Common Lisp did not exist at all until about a decade later. Their "Pure Lisp" language was (I am guessing) instead based on MACLISP, which is the mainline predecessor of Common Lisp. The later version of their system, still available for download, definitely is on top of Common Lisp. But when they presented the system at IJCAI in 1973, there wasn't even any idea of "Common Lisp". Later work in the early 1980s could have used something aspirationally called "Common Lisp"; Common Lisp was first defined in 1984 (and the more formal ANSI definition in 1994).

I propose that this historical niggle should be resolved by changing the word "Common Lisp" in the article to "Lisp". It might also be nice to provide a link to the last version (which is in Common Lisp) of NQTHM on Github: https://github.com/John-Nagle/nqthm Dicirnah (talk) 19:51, 22 October 2017 (UTC)

Yes, just go with "LISP". It originally ran on INTERLISP, on DEC PDP-10 family machines, at SRI International in Menlo Park. (That's OR, unless someone finds a good source. It probably is in "A Computational Logic", the book.) It was later ported to Franz LISP (by me) and then to Common LISP (by Boyer and Moore). There are links to the later versions at the end of the article. I put it on Github, making only some very minor changes because Common LISP has added some reserved words since the 1990s and there were name clashes. That got it running again, so now anyone can run one of the classics of AI. It's great to see it running several thousand times faster than it did in the PDP-10 days. John Nagle (talk) 20:39, 22 October 2017 (UTC)