The Coq mailing list

["Jean.Goubault-Larrecq" <Jean.Goubault AT dyade.fr>]

Emmanuel Ledinot wrote:
> Your problem is likely to be more easily tractable with a BDD-based boolean
> computation package, rather than with a theorem prover like Coq.

        In fact, there is no reason to make a choice here between
BDDs and Coq, as there is at least one BDD package in Coq.  It
was written last year by Kumar Neeraj Verma.  At that time, it
had everything to decide propositional formulae in classical logic,
and Kumar added a garbage collector this year.  It is complete
with sharing, memoizing functions, and so on.  All this runs
inside the lambda-calculus of Coq itself, so that you can use
it as part of your proof process.  However, you have to know
that this is not quite a push-button solution (no fancy notations
or interfaces...)
        Kumar is currently working on adding propositional
quantification and building a full certified symbolic
model-checker for the modal mu-calculus running entirely inside
Coq's lambda-calculus.
        Ask me or Kumar (for now you can contact him at
csu96139 AT cse.iitd.ernet.in)
 about it.
        All the best,

        -- Jean.