[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
quantifier library
*****
hi,
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 ?
thanks,
------------------------------------------------------------
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
------------------------------------------------------------