@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},
)