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; Sun, 15 Jan 1995 14:09:32 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA11170; Sun, 15 Jan 1995 07:01:19 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from canopus.cc.umanitoba.ca by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA11165; Sun, 15 Jan 1995 07:01:17 -0700 Received: from eeserv.ee.UManitoba.CA (root@eeserv.ee.umanitoba.ca [130.179.8.1]) by canopus.cc.umanitoba.ca (8.6.9/8.6.9) with SMTP id HAA22909 for ; Sun, 15 Jan 1995 07:59:10 -0600 Received: from brandy.ee.umanitoba.ca.umeeng by eeserv.ee.UManitoba.CA (4.1/25a-eef) id AA09035; Sun, 15 Jan 95 07:59:04 CST From: Budi Rahardjo Message-Id: <9501151359.AA09035@eeserv.ee.UManitoba.CA> Subject: tautology checker algorithms? To: info-hol@leopard.cs.byu.edu (Info HOL) Date: Sun, 15 Jan 1995 07:59:03 -0600 (CST) X-Mailer: ELM [version 2.4 PL22] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 596 Howdy, 1. What is the algorithm used in `taut`, the tautology checker library? Is there a documentation/reference for this? Is it possible to use BDD within HOL for this purpose? [I am only aware of the works at UBC] 2. I am looking for a library/theorem to manipulate propositional or first order tableaux. Is there such a beast? It would be nice if it can visually display the tableaux (upon request). thanks -- budi -- Budi Rahardjo Electrical and Computer Engineering - University of Manitoba - Canada