Re: [isabelle] bdd formalization

Hello Yongjian Li,

We have recently done such a formalization for BDDs in Isabelle/HOL. A description of it is given in a paper published in FM'2012:

The only available version on this page is still Isabelle 2011 but we also have updated it for Isabelle 2012, and we plan to submit it to the AFP sooner or later.

It is based on the Imperative_HOL theory provided in the Isabelle/HOL's library and thus uses a monad to model the imperative statements.

It also uses the Isabelle Collection Framework available on the AFP.

I hope it will correspond to your wishes. Please ask any further question you could have about it.


- Mathieu

IRIT, Université Paul Sabatier
Toulouse, France

Le 28/10/2012 02:24, yongjian Li a écrit :
dear experts:
    Who know good bdd formalization. I remember HOL4 theorem prover have good support in bdd.

   I know Schirmer's formal account and proof of bdd normalization, but it seems that this formalization does not fit my need well.

   what I need: semantically judge whether a boolean function is equal to False; besides, I also need know its structure:
whether it is a Var or boolean conjunction, or disjunction.

   In short, a bdd formalization should be a normal form of boolean functions.

   If you are intersting, please see the attcahed paper, please see fig1 and 3. I want to formalize and prove these algorithms.
what I need is the support for such an formalization.


Yongjian Li
Laboratory of Computer Science
Institute of Software
Chinese Academy of Sciences
P.O.Box 8718, Beijing 100080
Fax:  86-10-62661627

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.