Email Gateway (Aug 18 2022 at 18:11): Email Gateway (Aug 18 2022 at 18:11):From: Johannes Faber <johannesfaber@gmx.de>
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.
Many thanks for any help!
Johannes
smime.p7s
Email Gateway (Aug 18 2022 at 18:11):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 25 2024 at 16:19 UTC