[isabelle] bdd formalization



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

Attachment: fmcad07.pdf
Description: Binary data

BEGIN:VCARD
VERSION:2.1
N:yongjian Li;
FN:yongjian Li
ORG:Laboratory of Computer Science, , Institute of Software, Chinese Academy of 
 Sciences
TEL;HOME;VOICE:86-10-62664638
TEL;CELL;VOICE:86-10-62661638
ADR;HOME;POSTAL;PARCEL:;;4# South Fourth Street, Zhongguan Cun, Beijing, China;B
 eijing;;100080;China
LABEL;HOME;ENCODING=QUOTED-PRINTABLE:4# South Fourth Street, Zhongguan Cun, Beijing, China
Beijing

100080
China
EMAIL;PREF;INTERNET:lyj238 at ios.ac.cn
REV:20121028T092427Z
END:VCARD


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