Re: [isabelle] formal verification for nonmonotonic logics

There is a formalisation of Craig's Interpolation Theorem for a sequent style system available at

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.


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> |

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