[isabelle] formal verification for nonmonotonic logics
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  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,
 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