@article {IOPORT.05898609,
    author       = {Cantone, Domenico and Felici, Massimo and Nicolosi Asmundo, Marianna},
    title        = {Solvable set/hyperset contexts. III. A tableau system for a fragment of hyperset theory.},
    year         = {2010},
    journal      = {Rendiconti dell'Istituto di Matem\`atica dell'Universit\'a di Trieste},
    volume       = {42},
    issn         = {0049-4704},
    pages        = {165-190},
    publisher    = {Istituto di Matem\`atica, Universit\`a di Trieste, Trieste},
    abstract     = {Summary: We propose a decision procedure for a fragment of the hyperset theory, HMLSS, which takes inspiration from a tableau saturation strategy presented in [{\it D. Cantone}, ``A fast saturation strategy for set-theoretic tableaux", Lect. Notes Comput. Sci. 1227, 122--137 (1997; Zbl 0939.00022)] 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. For Part II see [{\it A. Dovier}, {\it E. G. Omodeo} and {\it A. Policriti}, Appl. Algebra Eng. Commun. Comput. 9, No. 4, 293--332 (1999; Zbl 0936.68025)].},
    identifier   = {05898609},
}