Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory

TL;DR

This paper formalizes and verifies a decision procedure for a quantifier-free set theory fragment using Isabelle/HOL, including a tableau calculus, executable implementation, and a type system extension for integration.

Contribution

It introduces a verified tableau-based decision procedure for MLSS set theory fragment within Isabelle/HOL, including formalization, proof of correctness, and implementation.

Findings

Verified the decision procedure's correctness and termination.

Formalized the syntax, semantics, and tableau calculus for MLSS.

Extended calculus with a type system for integration into Isabelle/HOL.

Abstract

Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a quantifier-free fragment of set theory. We formalise its syntax and semantics as well as a sound and complete tableau calculus for it. We also provide an executable specification of a decision procedure that exhaustively applies the rules of the calculus and prove its termination. Furthermore, we extend the calculus with a lightweight type system that paves the way for an integration of the procedure into Isabelle/HOL.