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.
IRIT, Université Paul Sabatier
Le 28/10/2012 02:24, yongjian Li a écrit :
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.
Laboratory of Computer Science
Institute of Software
Chinese Academy of Sciences
P.O.Box 8718, Beijing 100080
This archive was generated by a fusion of
Pipermail (Mailman edition) and