Towards a Verified Prover for a Ground Fragment of Set Theory
share
Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a ground fragment of set theory. We formalise the syntax and semantics of MLSS as well as a sound and complete tableau calculus for it. We also provide an abstract specification of a decision procedure that applies the rules of the calculus exhaustively and prove its termination.
READ FULL TEXT