*To*: Сергей Каунов <skaunov at gmail.com>*Subject*: Re: [isabelle] Sequents evaluation*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Tue, 22 Dec 2009 11:13:13 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1261464065.2897.28.camel@serge-desktop>*References*: <1261464065.2897.28.camel@serge-desktop>

Hello Sergei, most textbook presentations of proofs in modal and temporal logics are based on either Hilbert-style or sequent-style proof systems, neither of which are well supported in Isabelle. (The formalization of sequents as an Isabelle object logic that you refer to is quite old and has, AFAIK, not evolved since at least a decade; it is not supported by Isabelle's efficient automatic proof methods.) An alternative is to embed the "forcing" relation "sigma |= phi" (phi holds over structure sigma) in one of the well-developed object logics of Isabelle such as Isabelle/HOL, and to define validity "|= phi" as "\<forall> sigma. sigma |= phi". For example, for linear-time temporal logic, sigma would be an infinite sequence of states, which themselves are valuations of atomic propositions. You would then define the semantics of operators such as X (next time) and G (always) according to their standard definition over sequences. From these you can derive standard LTL laws such as |= (G phi) <=> phi /\ XG phi within the representation of LTL. Branching-time temporal logics can be handled similarly. This approach has been followed several times. You may want to look at sessions "Modelcheck" or "Unity" in the HOL library for similar formalizations. (My own "TLA" embedding is related, but stupidly based on an axiomatic rather than definitional approach to defining temporal operators.) If you are interested, I could send you (off-list) a simple embedding of LTL in HOL. Best regards, Stephan On 22 Dec 2009, at 07:41, Сергей Каунов wrote: > Hello! > > I'm sorry for disturbing you with the question, which may be quite > silly. I want to use Isabelle for some very simple temporal reasoning by > modal logic. Neither S4, neither Modal0 nor other modal thys aren't > covered in logics.pdf. ☹ > I starred on corresponding files and twisted them as I could, but didn't > found any natural way to evaluate propositions in Sequents logic. Is > there some hidden door, walkaround or a simple decision I missed? > > Thanks in advance! > -- > Сергей Каунов <skaunov at gmail.com> > > -- Stephan Merz, INRIA Nancy & LORIA Stephan.Merz at loria.fr

**References**:**[isabelle] Sequents evaluation***From:*Сергей Каунов

- Previous by Date: [isabelle] Sequents evaluation
- Next by Date: [isabelle] typeclasses?
- Previous by Thread: [isabelle] Sequents evaluation
- Next by Thread: [isabelle] typeclasses?
- Cl-isabelle-users December 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list