Email Gateway (May 18 2023 at 13:27): Email Gateway (May 18 2023 at 13:27):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new AFP entry, MLSS Decision Procedure, by Lukas Stevens:
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.
Now on-line at https://www.isa-afp.org/entries/MLSS_Decision_Proc.html
Larry
Last updated: Apr 25 2024 at 20:15 UTC