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; Thu, 26 May 1994 16:58:39 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25170; Thu, 26 May 1994 09:37:02 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25166; Thu, 26 May 1994 09:36:52 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Thu, 26 May 1994 17:32:20 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <10099-0@i80fs2.ira.uka.de>; Thu, 26 May 1994 17:38:41 +0200 Date: Thu, 26 May 94 17:38:39 EDT From: reetz To: hol2000@leopard.cs.byu.edu, garrel@msiadmin.cit.cornell.edu Subject: RERE:rewrite as primitive? Message-Id: <"i80fs2.ira.101:26.04.94.15.38.45"@ira.uka.de> >What is a bdd-package? Well, I just used a "shortage" for the following: for some sorts of decidable logics (e.g. LTL, CTL) there are provers based on decision diagrams, mostly on ordered binary decision diagrams (OBDD or BDD for short). If one encounters a subgoal during proving, which belongs to that sort of logics, the hol term is translated into the format of that bdd-based prover, written out of hol and proven by that prover. bdd-package normaly stands for a library for manipulating bdd's, that are heavily used by that prover. There already exists works on that (I don't have all the HOL-Proccedings right here...one name was HOL-VOSS, I think, but I might be awfully wrong) Ralf.