### Abstract

This formalization verifies a decision procedure due to Cantone and Zarba for a quantifier-free fragment of set theory.
The fragment is called multi-level syllogistic with singleton, or MLSS for short.
Its syntax syntax includes the usual set operations union, intersection, difference, membership, equality as well as the construction of a set containing a single element.
We specify the semantics of MLSS in terms of hereditarily finite sets and provide a sound and complete tableau calculus for it.
We also provide an executable specification of a decision procedure that applies the rules of the calculus exhaustively and prove its termination.
Furthermore, we extend the calculus with a light-weight type system that paves the way for an integration of the procedure into Isabelle/HOL.

### License

### Topics

- Logic/General logic/Classical propositional logic
- Logic/Set theory
- Logic/General logic/Decidability of theories

### Related publications

- Stevens, L. (2022).
*Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory*(Version 2). arXiv. https://doi.org/10.48550/ARXIV.2209.14133

### Session MLSS_Decision_Proc

- MLSS_Logic
- MLSS_HF_Extras
- MLSS_Realisation
- MLSS_Semantics
- MLSS_Typing_Defs
- MLSS_Calculus
- MLSS_Typing
- MLSS_Proc
- MLSS_Suc_Theory
- MLSS_Typing_Urelems
- MLSS_Proc_Code
- MLSS_Proc_All