[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