[isabelle] [Fwd: Re: formal verification for nonmonotonic logics]

--- Begin Message ---
You should look at
where the completness of a sequent system for first-order logic is proved. If your system is non-propositional, the question of how to handle bound variables arises. The above work uses de Bruijn indices but a nicer approach is the nominal one due to Christian Urban:


Yarden Katz wrote:
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,

[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.
Yarden Katz <yarden at umd.edu> | www.mindswap.org/~katz

--- End Message ---

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