Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Default reasoning


view this post on Zulip Email Gateway (Aug 18 2022 at 10:35):

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: May 03 2024 at 08:18 UTC