From: Klaus Ostermann <ostermann@informatik.tu-darmstadt.de>
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?
Regards,
Klaus
Last updated: Nov 21 2024 at 12:39 UTC