Complexity Assessments for Decidable Fragments of Set Theory. I : A Taxonomy for the Boolean Case

• Autorzy: Cantone Domenico , De Domenico Andrea , Maugeri Pietro , Omodeo Eugenio G.

Identyfikatory

DOI

10.3233/FI-2021-2050

• Języki publikacji: EN

Abstrakty

EN

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, \, the Boolean relators ⊆, ⊈,=, ≠, and the predicates ‘• = Ø’ and ‘Disj(•, •)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘• ≠ Ø and ‘¬Disj(•, •)’. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

Słowa kluczowe

EN

satisfiability problem; computable set theory; Boolean set theory; expressibility; NP-completeness; proof verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 181, nr 1
• Strony: 37--69
• Opis fizyczny: Bibliogr. 34 poz., tab.

Twórcy

autor

Cantone Domenico

• Dept. of Mathematics and Computer Science, University of Catania, Italy

autor

De Domenico Andrea

• Scuola Superiore di Catania, University of Catania, Italy

autor

Maugeri Pietro

• Dept. of Mathematics and Computer Science, University of Catania, Italy

autor

Omodeo Eugenio G.

• Dept. of Mathematics and Geosciences, University of Trieste, Italy

Bibliografia

• [1] Schwartz JT. Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. Technical Report 78-10, NASA Langley Research Center, Hampton, Virginia, 1978.
• [2] Cantone D, Ferro A, Omodeo EG. Computable set theory. Number 6 in International Series of Monographs on Computer Science, Oxford Science Publications. Clarendon Press, Oxford, UK, 1989.
• [3] Cantone D, Omodeo EG, Policriti A. Set theory for computing - From decision procedures to declarative programming with sets. Monographs in Computer Science. Springer-Verlag, New York, 2001.
• [4] Schwartz JT, Cantone D, Omodeo EG. Computational logic and set theory: Applying formalized logic to analysis. Springer-Verlag, 2011. ISBN 978-0-85729-807-2. doi:10.1007/978-0-85729-808-9. Foreword by M. Davis.
• [5] Omodeo EG, Policriti A, Tomescu AI. On Sets and Graphs: Perspectives on Logic and Combinatorics. Springer, 2017. ISBN 978-3-319-54981-1. URL https://link.springer.com/book/10.1007%2F978-3-319-54981-1.
• [6] Cantone D, Ursino P. An Introduction to the Technique of Formative Processes in Set Theory. Springer International Publishing, 2018. ISBN 978-3-319-74778-1. doi:10.1007/978-3-319-74778-1.
• [7] Ferro A, Omodeo EG, Schwartz JT. Decision procedures for some fragments of Set Theory. In: Proceedings of CADE-5, Les Arcs, France, July 8-11, 1980, volume 87 of LNCS. Springer-Verlag, 1980 pp. 88-96.
• [8] Ferro A, Omodeo EG, Schwartz JT. Decision Procedures for Elementary Sublanguages of Set Theory. I: Multilevel Syllogistic and Some Extensions. Commun. Pur. Appl. Math., 1980. 33:599-608.
• [9] Breban M, Ferro A, Omodeo E, Schwartz J. Decision Procedures for Elementary Sublanguages of Set Theory. II: Formulas involving Restricted Quantifiers, together with Ordinal, Integer, Map, and Domain Notions. Commun. Pur. Appl. Math., 1981. 34:177-195.
• [10] Cantone D, Cutello V, Policriti A. Set-theoretic reductions of Hilbert’s Tenth Problem. In: Börger E, Büning HK, Richter MM (eds.), CSL ’89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings, volume 440 of LNCS. Springer, 1990 pp. 65-75.
• [11] Cantone D, Omodeo EG, Panettiere M. From Hilbert’s 10th problem to slim, undecidable fragments of set theory. In: Cordasco G, Gargano L, Rescigno A (eds.), Proceedings of the 21st Italian Conference on Theoretical Computer Science, ICTCS 2020, Ischia, Italy, September 14-16, 2020, CEUR Workshop Proceedings. CEUR-WS.org, To appear.
• [12] Cantone D, Omodeo EG, Policriti A. The Automation of Syllogistic. II: Optimization and Complexity Issues. J. Automat. Reasoning, 1990. 6(2):173-187.
• [13] Cantone D. Decision procedures for elementary sublanguages of Set Theory. X. Multilevel syllogistic extended by the singleton and powerset operators. J. Automat. Reasoning, 1991. 7(2):193-230.
• [14] Cantone D, Omodeo EG, Ursino P. Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators. Inform. Comput., 2002. 172(2):165-201. doi:10.1006/inco.2001.3096.
• [15] Cantone D, Ursino P. Formative processes with applications to the decision problem in set theory. II: Powerset and singleton operators, finiteness predicate. Inform. Comput., 2014. 237:215-242.
• [16] Cantone D, Zarba CG. A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra R, Salzer G (eds.), Automated Deduction in Classical and Non-Classical Logics, volume 1761 of LNAI, pp. 127-137. Springer-Verlag, 2000.
• [17] Omodeo EG, Tomescu AI. Set graphs. III. Proof Pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. J. Automat. Reasoning, 2014. 52(1):1-29.
• [18] Cantone D, Maugeri P, Omodeo EG. Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership. Theoretical Computer Science, 2020. doi:https://doi.org/10.1016/j.tcs.2020.08.023. URL http://www.sciencedirect.com/science/article/pii/S0304397520304825.
• [19] Cantone D, De Domenico A, Maugeri P, Omodeo EG. A quadratic reduction of constraints over nested sets to purely Boolean formulae in CNF. In: Calimeri F, Perri S, Zumpano E (eds.), Proceedings of the 35th Italian Conference on Computational Logic, Rende, Italy, October 13-15, 2020, volume 2710 of CEUR Workshop Proceedings. CEUR-WS.org, 2020 pp. 214-230. ISSN 1613-0073.
• [20] Jacobson N. Lectures in Abstract Algebra, Vol.1 - Basic Concepts. D. Van Nostrand, New York, 1951.
• [21] Manin YI. A course in mathematical logic. Graduate texts in Mathematics. Springer-Verlag, 1977.
• [22] Garey MR, Johnson DS. Computers and Intractability: A Guide to the Theory of NP-Completeness. Series of Books in the Mathematical Sciences. W. H. Freeman, 1979. ISBN 0716710455.
• [23] Cantone D, Maugeri P. Polynomial-Time Satisfiability Tests for ‘Small’ Membership Theories. In: Cherubini A, Sabadini N, Tini S (eds.), Proceedings of the 20th Italian Conference on Theoretical Computer Science, ICTCS 2019, Como, Italy, September 9-11, 2019, volume 2504 of CEUR Workshop Proceedings. CEUR-WS.org, 2019 pp. 261-273. URL http://ceur-ws.org/Vol-2504/paper29.pdf.
• [24] Cantone D, Domenico AD, Maugeri P, Omodeo EG. Polynomial-time satisfiability tests for Boolean fragments of Set Theory. In: Casagrande A, Omodeo EG (eds.), Proceedings of the 34th Italian Conference on Computational Logic, Trieste, Italy, June 19-21, 2019, volume 2396 of CEUR Workshop Proceedings. CEUR-WS.org, 2019 pp. 123-137. URL http://ceur-ws.org/Vol-2396/paper22.pdf.
• [25] Lewis HR. Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci., 1980. 21(3):317-353. URL https://doi.org/10.1016/0022-0000(80)90027-6.
• [26] Meier A, Thomas M, Vollmer H, Mundhenk M. The complexity of satisfiability for fragments of CTL and CTL*. Int. J. Found. Comput. Sci., 2009. 20(5):901-918. URL https://doi.org/10.1142/S0129054109006954.
• [27] Bozzelli L, Molinari A, Montanari A, Peron A, Sala P. Which fragments of the interval temporal logic HS are tractable in model checking? Theor. Comput. Sci., 2019. 764:125-144. URL https://doi.org/10.1016/j.tcs.2018.04.011.
• [28] Bozzelli L, Molinari A, Montanari A, Peron A, Sala P. Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy. Inf. Comput., 2018. 262(Part):241-264. URL https://doi.org/10.1016/j.ic.2018.09.006.
• [29] Stolzenburg F. Membership-Constraints and Complexity in Logic Programming with Sets. In: Baader F, Schulz KU (eds.), Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26-29, 1996, Proceedings, volume 3 of Applied Logic Series. Kluwer Academic Publishers, 1996 pp. 285-302.
• [30] Dovier A, Piazza C, Rossi G. A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. ACM Trans. Comput. Log., 2008. 9(3):15:1-15:30. URL https://doi.org/10.1145/1352582.1352583.
• [31] Cristiá M, Rossi G. Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations. J. Autom. Reason., 2020. 64(2):295-330. URL https://doi.org/10.1007/s10817-019-09520-4.
• [32] Dovier A, Pontelli E, Rossi G. Set unification. Theor. Pract. Log. Prog., 2006. 6(6):645-701. URL https://doi.org/10.1017/S1471068406002730.
• [33] Büttner W, Simonis H. Embedding Boolean Expressions into Logic Programming. J. Symb. Comput., 1987. 4(2):191-205. URL https://doi.org/10.1016/S0747-7171(87)80065-2.
• [34] Dovier A, Omodeo EG, Pontelli E, Rossi GF. A Language for Programming in Logic with Finite Sets. J. Logic Program., 1996. 28(1):1-44.