[isabelle] Question regarding sequent calculi in Isabelle




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

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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