Email Gateway (Aug 17 2022 at 14:46): Email Gateway (Aug 17 2022 at 14:46):From: Yarden Katz <yarden@umd.edu>
Hi all,
Let me preface my by declaring that I'm completely new to Isabelle.
I am interested in nonmonotonic logics, and I would like to formally
verify metatheorems in these systems -- in particular, for default
logic. Gerwin Klein suggested that it is in principle possible to do
this by defining a proof system for these logics within an existing
instantiation of Isabelle (e.g. Isabelle/HOL). My first thought is
to try doing this with one of the sequent calculi for default logic
(see [1] for skeptical variant of default logic). Does anyone have
any other hints on this -- especially how feasible it is within
Isabelle -- or pointers to existing work that is relevant?
Thanks a lot,
--Yarden
[1] Bonatti, P. A. and Olivetti, N. 1997. A Sequent Calculus for
Skeptical Default Logic. In Proceedings of the international
Conference on Automated Reasoning with Analytic Tableaux and Related
Methods (May 13 - 16, 1997). D. Galmiche, Ed. Lecture Notes In
Computer Science, vol. 1227. Springer-Verlag, London, 107-121.
Email Gateway (Aug 17 2022 at 14:46):From: Tom Ridge <Thomas.J.Ridge@cl.cam.ac.uk>
There is a formalisation of Craig's Interpolation Theorem for a sequent
style system available at
http://www.cl.cam.ac.uk/users/tjr22/doc.html
This might give some indication of how sequent style systems can be
formalised. My belief is that such proofs are feasible, regardless of
the representation of binding used. However, learning to use a theorem
prover in the first place is not routine.
Tom
Yarden Katz wrote:
Last updated: May 03 2024 at 08:18 UTC