Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Logic in Computer Science
2023-07-04 v2
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.
Keywords
Cite
@article{arxiv.2209.14133,
title = {Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory},
author = {Lukas Stevens},
journal= {arXiv preprint arXiv:2209.14133},
year = {2023}
}