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