Re: [isabelle] Quantifying over conditions
On Tue, 2011-02-08 at 10:46 +1300, Timothy McKenzie wrote:
> I don't know if this is precisely what you're looking for, but
> what you're asking for seems to have the flavour of modal logic:
> I don't know how easily this could be (or perhaps already has
> been) incorporated into Isabelle. Perhaps someone else could
> address that question.
(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/index.html) contains implementations of modal logics.
However, depending on John's application, it might be more appropriate
to define the modal operators in Isabelle/HOL. An extensive repository
that defines modal (and other) algebras is currently available at
This archive was generated by a fusion of
Pipermail (Mailman edition) and