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:
> http://en.wikipedia.org/wiki/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.

Isabelle/Sequents
(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
http://staffwww.dcs.shef.ac.uk/people/G.Struth/isa/

Kind regards,
Tjark






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