*To*: Johannes Faber <johannesfaber at gmx.de>*Subject*: Re: [isabelle] Question regarding sequent calculi in Isabelle*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 10 Aug 2011 11:27:22 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <17CE2470-6CAE-4622-8AA3-2CD337645919@gmx.de>*References*: <17CE2470-6CAE-4622-8AA3-2CD337645919@gmx.de>

I hesitate to call anything impossible, because there are various ways to attach code to a theory. However, this kind of systematic renaming of non-variable symbols isn't directly supported by Isabelle's logical framework. As for your second question, certainly most development focuses on Isabelle/HOL, but much of it involves strengthening the framework in general, which benefits all logics. We have retained a lot of ancient developments, such as CCL, and I would be very surprised if we got rid of the Sequents theory. Whether there exists an alternative out there I couldn't say. There are of course ready-made implementations of dynamic logic, http://www.key-project.org/ for example. Larry Paulson On 9 Aug 2011, at 10:34, Johannes Faber wrote: > > Hi all, > > I currently work on implementing a sequent-style proof calculus over dynamic logic. To this end, I have given Isabelle a try (which I haven't used much before) and extended LK0.thy from the Sequents logic with my proof rules. This seems to work until I run into problems with a symbolic execution rule, where every symbol in a predicate needs to be replaced by a new symbol. > > The rule is of the shape > > |- p[v0/v'] --> q[v0/v] > -----------------------, > |- [p]q > > where p[v0/v'] denotes the replacement of every primed symbol in p by a fresh symbol v0 (and similarly for q). This is not a problem as long as only a single symbol is to be substituted -- but I need to replace all primed symbols in v'. Is something like this possible with Isabelle? > > Second, I have a more general question: it seems that the Sequents theory of Isabelle isn't used much and that the main work is on Isabelle/HOL. Does it nevertheless make sense to use the Sequents theory of Isabelle as a basis for a sequent-style calculus, or is Isabelle not the right choice for such a calculus? > > I have already asked Makarius about this, who pointed me to this mailing list. > > On 10 Jul 2011, Makarius wrote: >> This looks a bit too "syntactic". The framework does not allow to access >> the term structure as such, you somehow need to reason symbolically within >> the minimal logic of Pure. >> >> There might be ways, say in Isabelle/HOL with a more detailed syntactic >> model of the calculus. But this also means you have to invest more work >> in the formalization. >> >> The Sequents theories are really old. I guess that quite a bit more >> expertise has emerged in the past decades how to do such things. If you >> ask on isbelle-users some experts might tell you more. > > > Many thanks for any help! > > Johannes > > -- > Dipl.-Inform. Johannes Faber > Correct System Design Group > Department of Computing Science > Carl von Ossietzky University of Oldenburg > Phone: +49 441 798-4638 > Fax: +49 441 798-2965

**References**:**[isabelle] Question regarding sequent calculi in Isabelle***From:*Johannes Faber

- Previous by Date: Re: [isabelle] schematic variables
- Next by Date: Re: [isabelle] schematic variables
- Previous by Thread: [isabelle] Question regarding sequent calculi in Isabelle
- Next by Thread: [isabelle] Scala Code Generation
- Cl-isabelle-users August 2011 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