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 10:14:10 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA11972; Mon, 16 Jan 1995 03:02:40 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA11968; Mon, 16 Jan 1995 03:02:34 -0700 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 16 Jan 1995 09:59:30 +0000 To: Budi Rahardjo Cc: info-hol@leopard.cs.byu.edu (Info HOL), Richard.Boulton@cl.cam.ac.uk Subject: Re: tautology checker algorithms? In-Reply-To: Your message of "Sun, 15 Jan 1995 07:59:03 CST." <9501151359.AA09035@eeserv.ee.UManitoba.CA> Date: Mon, 16 Jan 1995 09:59:21 +0000 From: Richard Boulton Message-Id: <"swan.cl.cam.:022440:950116095937"@cl.cam.ac.uk> Budi Rahardjo writes: > 1. What is the algorithm used in `taut`, the tautology checker library? > Is there a documentation/reference for this? There is documentation for the library in the sources: hol88/Library/taut/Manual/ hol90.7/library/taut/Manual/ This includes an informal description of the algorithm used. I am not aware of any other references. > 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): J. Harrison "Binary Decision Diagrams as a HOL Derived Rule" In "Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 1994", T. F. Melham and J. Camilleri (Eds.), pages 254--268, Lecture Notes in Computer Science volume 859, Springer-Verlag. Contact jrh@cl.cam.ac.uk for more information. > 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). There is a tool called FAUST which might help. Take a look at: R. Kumar, Th. Kropf, and K. Schneider "Integrating a First-Order Automatic Prover in the HOL Environment" In "Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL91), Davis, California, August 1991", M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (Eds.), pages 170--176, IEEE Computer Society Press. Perhaps one of the Karlsruhe people would like to comment on this? Richard Boulton University of Cambridge Computer Laboratory