Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <26528-0@swan.cl.cam.ac.uk>; Fri, 10 Apr 1992 23:36:15 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05594; Fri, 10 Apr 92 15:27:10 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from cli.com by ted.cs.uidaho.edu (16.6/1.34) id AA05590; Fri, 10 Apr 92 15:27:04 -0700 Received: by CLI.COM (4.1/1); Fri, 10 Apr 92 17:24:12 CDT Date: Fri, 10 Apr 92 17:26:17 CDT From: Matt Kaufmann Message-Id: <9204102226.AA07475@thunder.CLI.COM> Received: by thunder.CLI.COM (4.1/CLI-1.2) id AA07475; Fri, 10 Apr 92 17:26:17 CDT To: info-hol@edu.uidaho.cs.ted, nqthm-users@com.cli Cc: archer@edu.ucdavis.cs, gfink@edu.ucdavis.cs, kaufmann@com.cli Subject: connecting HOL with the Boyer-Moore Theorem Prover Is there much serious interest out there in connecting the Boyer-Moore Theorem Prover with HOL? What I have in mind (and what I believe is similar to what Myla Archer and some others at UC Davis have been looking into) is some kind of connection that allows you to ship off certain HOL goals to the Boyer-Moore Theorem Prover, which is a ``first-order'' prover that has induction and natural number linear arithmetic. (An extension has some weak support for first-order quantification and an interactive goal-directed assistant much like HOL's.) Without saying more right now (such as who might get involved in the implementation, just how the mechanism might work, or how to address soundness), I'd like to pose the following request/challenge: Provide explicit examples of HOL theorems (possibly in the context of a theory) for which the Boyer-Moore theorem prover might provide useful assistance. I'd be very interested in seeing such examples. You could send them by email to me, Matt Kaufmann, at kaufmann@cli.com . Thanks.