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]qwhere 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 withinthe 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 workin the formalization. The Sequents theories are really old. I guess that quite a bit moreexpertise has emerged in the past decades how to do such things. If youask 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
Description: S/MIME cryptographic signature