Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Mon, 3 May 93 12:40:08 CDT
From: Matt Kaufmann <kaufmann@cli.com>
Message-Id: <9305031740.AA01218@thunder.CLI.COM>
To: info-hol@ted.cs.uidaho.edu
In-Reply-To: Mike Coe's message of Mon, 3 May 93 9:59:12 PDT <9305031659.AA08710@leopard.cs.uidaho.edu>
Subject: help

Regarding ``debugging'' of non-theorems......

Here is what happens if one tries the recently-proposed non-theorem

((t-1)+1) = t

in the Boyer-Moore prover.  I'll add comments to the transcript --
comments occur from any semicolon to the end of the line.  Do HOL
users sometimes find that HOL can provide help on failed theorems, in
the sense shown below?

thunder:kaufmann[108]% nqthm-1992
AKCL (Austin Kyoto Common Lisp)  Version(1.615) Thu Dec 17 14:43:43 CST 1992
Contains Enhancements by W. Schelter

Nqthm-1992.
Initialized with (BOOT-STRAP NQTHM) on February 24, 1993  15:43:58.
>(prove-lemma mistake ()
   (implies (numberp x) ;; presumably this "type" is inferred in HOL
	    (equal (plus (difference x 1) 1)
		   x)))

This simplifies, using linear arithmetic, to the goal:

;; Presumably the theorem prover has internally handled the case
;; where X is positive, since it simplifies the goal above to:

      (IMPLIES (AND (EQUAL X 0) (NUMBERP X))
               (EQUAL (PLUS (DIFFERENCE X 1) 1) X)).

This again simplifies, expanding NUMBERP, DIFFERENCE, PLUS, and EQUAL, to the
formula:

      F.

Need we go on?

************** F  A  I  L  E  D **************


[ 0.0 0.0 0.0 ]
NIL

;; We can enter an execution loop for the Boyer-Moore logic to see
;; what went wrong in the case X = 0.  Note:  Everything here is
;; case-INsensitive.

>(r-loop)

Trace Mode: Off   Abbreviated Output Mode:  On
Type ? for help.
*(let ((x 0)) ;; "Let x = 0 in...."
   (PLUS (DIFFERENCE X 1) 1))
 1
;; Perhaps the above is surprising, so let's focus on a subterm:
*(let ((x 0))
   (DIFFERENCE X 1))
 0
*

-- Matt Kaufmann