Email Gateway (Aug 19 2022 at 08:52): Email Gateway (Aug 19 2022 at 08:52):From: yongjian Li <lyj238@ios.ac.cn>
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.
regards
Yongjian Li
Laboratory of Computer Science
Institute of Software
Chinese Academy of Sciences
P.O.Box 8718, Beijing 100080
P.R. CHINA
Tel:86-10-62661658
Fax: 86-10-62661627
2012-10-28
fmcad07.pdf
yongjian Li(3).vcf
Email Gateway (Aug 19 2022 at 08:54):From: Mathieu Giorgino <Mathieu.Giorgino@irit.fr>
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:
http://www.irit.fr/~Mathieu.Giorgino/Publications/GiSt2012BDD.html
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.
Regards,
IRIT, Université Paul Sabatier
Toulouse, France
Last updated: Nov 21 2024 at 12:39 UTC