| ||||
| ||||
![]() Title:Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory Authors:Lukas Stevens Conference:CADE-29 Tags:Decision procedures, Proof assistants, Set theory and Tableau 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 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. Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory ![]() Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory | ||||
Copyright © 2002 – 2025 EasyChair |