Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*
DOI10.3233/FI-2021-2050zbMath1498.03112OpenAlexW3177543793MaRDI QIDQ5158658
Pietro Maugeri, Domenico Cantone, Andrea de Domenico, Eugenio Giovanni Omodeo
Publication date: 25 October 2021
Published in: Fundamenta Informaticae (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.3233/fi-2021-2050
NP-completenessexpressibilitysatisfiability problemproof verificationcomputable set theoryBoolean set theory
Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Axiomatics of classical set theory and its fragments (03E30)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators
- Embedding Boolean expressions into logic programming
- Complexity results for classes of quantificational formulas
- Which fragments of the interval temporal logic HS are tractable in model checking?
- Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
- The automation of syllogistic. II: Optimization and complexity issues
- Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators
- Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership
- Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
- {log}: A language for programming in logic with finite sets
- Set unification
- THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
- Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
- Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
- An Introduction to the Technique of Formative Processes in Set Theory
- Computational Logic and Set Theory
- A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
- On Sets and Graphs
This page was built for publication: Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*