Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 27 Sep 1993 10:06:20 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02865; Mon, 27 Sep 93 01:55:17 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA02861; Mon, 27 Sep 93 01:55:10 -0700 Received: from skua.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 27 Sep 1993 09:54:35 +0100 To: shb@oracorp.com Cc: info-hol@cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk Subject: Re: C/HOL90 communication In-Reply-To: Your message of "Fri, 24 Sep 93 09:46:36 EDT." <9309241346.AA11970@sparta.oracorp.com> Date: Mon, 27 Sep 93 09:54:23 +0100 From: Wai Wong Message-Id: <"swan.cl.cam.:176500:930927085440"@cl.cam.ac.uk> Steve Said: > What's the simplest and/or most robust technique people can suggest > for having a C program find out whether a particular theorem is in a > HOL90 theory? One can assume that if the theorem is present then it > has a name known to the C program, if that helps. Given that the C program knows the name of the theorem and the theory it is in, it can spawn a HOL90 process to try to load the theorem and pipe the output of HOL90 to a simple recognizer to see whether the loading of the theorem is successful. The recognizer could be just a simple grep or perl script which looks for HOL90 failure message and returns a value according to the result. Since this method relies on HOL90 to find the theorem, it is simple and it is secure. Wai