In the fully expansive (or LCF-style) approach to theorem proving, theorems are represented by an abstract type whose primitive operations are the axioms and inference rules of a logic. Theorem proving tools are implemented by composing together the inference rules using ML programs.
This idea can be generalised to computing valid judgements that represent other kinds of information. In particular, consider judgements (a,r,t,b), where a is a set of boolean terms (assumptions) that are assumed true, r represents a variable order, t is a boolean term all of whose free variables are boolean and b is a BDD. Such a judgement is valid if under the assumptions a, the BDD representing t with respect to r is b, and we will write a r t --> b when this is the case.
The derivation of "theorems" like a r t --> b can be viewed as "proof" in the style of LCF by defining an abstract type term_bdd that models judgements a r t --> b analogously to the way the type thm models theorems |- t.
HolBddLib Version 2 provides a kernel of representation judgement rules as infrastructure for building fully-expansive combinations of HOL theorem proving and BDD-based symbolic calculation algorithms. All higher level tools, such as model checkers, are programmed in ML as derived rules.
HolBddLib currently contains two main structures: PrimitiveBddRules which defines a protected type term_bdd and rules for generating values of this type, and DerivedBddRules that contains derived rules for performing simple fixed-point calculations. There is also a theory DerivedBddRulesTheory containing the theorems on reachability and fixed points needed by the derived rules, and two small subsidiary structures Varmap and PrintBdd.
The development of HolBddLib has gone through two phases. The first phase consisted in experiments with different ways of linking higher order logic terms to binary decision diagrams. These are described in the paper Reachability programming in HOL98 using BDDs.
HolBddLib Version 2 provides a less developed interactive programming environment than Version 1. It is more oriented to providing a clean and simple API allowing implementers to create their own combinations of model checking and theorem proving. Such a combination could be a Voss-like verification platform.
MICHAEL J. C. GORDON