@article(BBRT18, author = {K.~Bansal and C.~W. Barrett and A.~Reynolds and C.~Tinelli}, year = {2018}, title = {Reasoning with Finite Sets and Cardinality Constraints in SMT}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {4}, pages = {1--31}, doi = {10.23638/LMCS-14(4:12)2018}, ) @(BST10, author = {C.~Barrett and A.~Stump and C.~Tinelli}, year = {2010}, title = {The Satisfiability Modulo Theories Library}, url = {http://www.smtlib.org}, ) @inproceedings(BGNRZ06, author = {M.P. Bonacina and S.~Ghilardi and E.~Nicolini and S.~Ranise and D.~Zucchelli}, year = {2006}, title = {Decidability and undecidability results for {N}elson-{O}ppen and rewrite-based decision procedures}, editor = {U.~Furbach and N.~Shankar}, booktitle = {Automated Reasoning. IJCAR 2006}, series = {Lecture Notes in Computer Science}, volume = {4130}, pages = {513--527}, doi = {10.1007/11814771\_42}, ) @book(BradleyManna2007, author = {Aaron~R. Bradley and Zohar Manna}, year = {2007}, title = {The calculus of computation - decision procedures with applications to verification}, publisher = {Springer}, doi = {10.1007/978-3-540-74113-8}, ) @article(CFS87, author = {D.~Cantone and A.~Ferro and J.T. Schwartz}, title = {Decision procedures for elementary sublanguages of set theory. {V}: {M}ultilevel syllogistic extended by the general union operator}, journal = {Journal of Computer and System Sciences}, number = {1}, pages = {1--18}, doi = {10.1016/0022-0000(87)90001-8}, ) @article(CFS85, author = {D.~Cantone and J.~T. Schwartz and A.~Ferro}, title = {Decision procedures for elementary sublanguages of set theory. VI. Multi-level syllogistic extended by the powerset operator}, journal = {Communications on Pure and Applied Mathematics}, number = {5}, pages = {549--571}, doi = {10.1002/cpa.3160380507}, ) @article(CanCut89b, author = {Domenico Cantone and Vincenzo Cutello}, year = {1989}, title = {Decision procedures for elementary sublanguages of Set Theory. {XVI}. {M}ultilevel syllogistic extended by singleton, rank comparison and unary intersection}, journal = {Bulletin of {EATCS}}, volume = {39}, pages = {139--148}, ) @article(CantoneDMO21, author = {Domenico Cantone and D{e Domenico}, Andrea and Pietro Maugeri and Eugenio~G. Omodeo}, year = {2021}, title = {Complexity Assessments for Decidable Fragments of Set Theory. {I}: A Taxonomy for the {B}oolean Case}, journal = {Fundamenta Informaticae}, volume = {181}, pages = {37--69}, doi = {10.3233/fi-2021-2050}, ) @book(CanFerOmo89a, author = {Domenico Cantone and Alfredo Ferro and Eugenio~G. Omodeo}, year = {1989}, title = {Computable set theory}, series = {International Series of Monographs on Computer Science, Oxford Science Publications}, volume = {6}, publisher = {Clarendon Press}, address = {Oxford, {UK}}, doi = {10.2307/2275351}, ) @article(CMO20, author = {Domenico Cantone and Pietro Maugeri and Eugenio~G. Omodeo}, title = {Complexity assessments for decidable fragments of set theory. {II:} {A} taxonomy for `small' languages involving membership}, journal = {Theoretical Computer Science}, pages = {28--46}, doi = {10.1016/j.tcs.2020.08.023}, ) @article(CanOmoPol90, author = {Domenico Cantone and Eugenio~G. Omodeo and Alberto Policriti}, year = {1990}, title = {The Automation of Syllogistic. {I}{I}: {O}ptimization and Complexity Issues}, journal = {J. Autom. Reasoning}, volume = {6}, number = {2}, pages = {173--187}, doi = {10.1007/BF00245817}, ) @book(CanOmoPol01, author = {Domenico Cantone and Eugenio~G. Omodeo and Alberto Policriti}, year = {2001}, title = {Set theory for computing - {\relax\fontsize {10}{12}\selectfont\abovedisplayskip 10\p@ plus2\p@ minus5\p@ \abovedisplayshortskip\z@ plus3\p@ \belowdisplayshortskip6\p@ plus3\p@ minus3\p@ \def\leftmargin \leftmargini\parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep5\p@ plus2\p@ minus5\p@ \itemsep2.5\p@ plus1.5\p@ minus\p@ {\leftmargin\leftmargini \topsep6\p@ plus2\p@ minus2\p@ \parsep3\p@ plus2\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip From decision procedures to declarative programming with sets}}, series = {Monographs in Computer Science}, publisher = {Springer-Verlag}, address = {New York}, doi = {10.1007/978-1-4757-3452-2}, ) @book(CanUrs18, author = {Domenico Cantone and Pietro Ursino}, year = {2018}, title = {An Introduction to the Technique of Formative Processes in Set Theory}, publisher = {Springer International Publishing}, doi = {10.1007/978-3-319-74778-1}, ) @article(FOS80b, author = {Alfredo Ferro and Eugenio~G. Omodeo and Jacob~T. Schwartz}, year = {1980}, title = {{D}ecision Procedures for Elementary Sublanguages of Set Theory. {I}: {M}ultilevel Syllogistic and Some Extensions.}, journal = {Comm. Pure Appl. Math.}, volume = {33}, pages = {599--608}, doi = {10.1002/cpa.3160330503}, ) @inproceedings(GNZ05, author = {S.~Ghilardi and E.~Nicolini and D.~Zucchelli}, year = {2005}, title = {A Comprehensive Framework for Combined Decision Procedures}, editor = {B.~Gramlich}, booktitle = {Frontiers of Combining Systems (FroCoS 2005)}, series = {Lecture Notes in Computer Science}, volume = {3717}, publisher = {Springer, Berlin, Heidelberg}, pages = {1--30}, doi = {10.1007/11559306\_1}, ) @article(NO79, author = {G.~Nelson and D.C. Oppen}, year = {1979}, title = {Simplification by cooperating decision procedures}, journal = {ACM Transactions on Programming Languages and Systems}, volume = {1}, number = {2}, pages = {245--257}, doi = {10.1145/357073.357079}, ) @inproceedings(RRZ05, author = {S.~Ranise and C.~Ringeissen and C.G. Zarba}, year = {2005}, title = {Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic}, editor = {B.~Gramlich}, booktitle = {Frontiers of Combining Systems (FroCoS 2005)}, series = {Lecture Notes in Computer Science}, volume = {3717}, publisher = {Springer, Berlin, Heidelberg}, pages = {48--64}, doi = {10.1007/11559306\_3}, ) @book(SchCanOmo11, author = {Jacob~T. Schwartz and Domenico Cantone and Eugenio~G. Omodeo}, year = {2011}, title = {Computational logic and set theory: Applying formalized logic to analysis}, publisher = {Springer-Verlag}, doi = {10.1007/978-0-85729-808-9}, note = {Foreword by M. Davis}, ) @inproceedings(MultiZarba02, author = {Calogero~G. Zarba}, title = {Combining Multisets with Integers}, editor = {Andrei Voronkov}, booktitle = {Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {363--376}, doi = {10.1007/3-540-45620-1\_30}, ) @article(Zarba05, author = {Calogero~G. Zarba}, title = {Combining Sets with Cardinals}, journal = {J. Autom. Reason.}, number = {1}, pages = {1--29}, doi = {10.1007/s10817-005-3075-8}, ) @inproceedings(Zarba02, author = {Calogero~G. Zarba}, title = {Combining Sets with Integers}, editor = {Alessandro Armando}, booktitle = {Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002, Proceedings}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {103--116}, doi = {10.1007/3-540-45988-X\_9}, )