Solvable Set/Hyperset Contexts: III. A Tableau System for a Fragment of Hyperset Theory

摘要

We propose a decision procedure for a fragment of the hyperset theory, HMLSS, which takes inspiration from a tableau saturation strategy presented in [3] for the fragment MLSS of well-founded set theory. The procedure alternates deduction and model checking steps, driving the correct application of otherwise very liberal rules, thus significantly speeding up the process of discovering a satisfying assignment of a given HMLSS-formula or proving that no such assignment exists.