Re: [isabelle] Question regarding sequent calculi in Isabelle

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, 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

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