[isabelle] formal verification for nonmonotonic logics

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

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