Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 16 Jan 1995 13:36:47 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA14425; Mon, 16 Jan 1995 06:22:37 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA14421; Mon, 16 Jan 1995 06:22:35 -0700 Received: from oberon.inmos.co.uk (oberon.inmos.co.uk [138.198.35.8]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id FAA27682 for ; Mon, 16 Jan 1995 05:20:16 -0800 Received: from frogland.inmos.co.uk by oberon.inmos.co.uk; Mon, 16 Jan 1995 13:20:12 GMT From: David Shepherd Message-Id: <25037.9501161313@frogland.inmos.co.uk> Subject: Re: tautology checker algorithms? To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Mon, 16 Jan 1995 13:13:50 +0000 (GMT) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1004 Richard Boulton has said: > Budi Rahardjo writes: > > > Is it possible to use BDD within HOL for this purpose? > > [I am only aware of the works at UBC] > > John Harrison has implemented a BDD procedure in HOL which is derived from > HOL's inference rules (as opposed to being built-in): Interestingly enough there is an SML-based BDD package described today in comp.lang.sml. It should be quite easy to base a simple (boolean) HOL90 BDD conversion/rule etc around this. With suitable code to automatically encode (finite) defined types then this could be extend further. -------------------------------------------------------------------------- david shepherd SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, u.k. tel/fax: +44 1454 611638/617910 email: des@inmos.co.u www: http://www.inmos.co.uk/~des/welcome.html "whatever you don't want, you don't want negative advertising"