[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

quantifier library


I am currently working on hardware verification. 
I am facing a problem of nested existential quantifier in 
the part of consequent. 

I have some questions,
Is there any library similar to unwind library in HOL ?
If not is there any library about the quantifier rules ?
or can anybody suggest me what is the best way to approach 
this problem ? 


Kong Woei Susanto
Department of Computing Science - University of Glasgow
17 LilyBank Gardens, Glasgow G12 8RZ. 
Phone: +44-141-3304454  Fax: +44-141-3304913
e-mail: susanto@dcs.gla.ac.uk / susanto@computer.org