[isabelle] Default reasoning

I'd like to formally specify and reason in (some variant of) default logic.

Is there any way to do this with Isabelle? For example, are there any object logics for this purpose
that can be downloaded somewhere?

Just to avoid misunderstandings: I do not want to prove any theorems about default logic, but I want to prove theorems about *theories* formulated in default logic, using the proof
rules of default logic.

If this is not possible with Isabelle, are there any other theorem provers
which support default reasoning?


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