Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate
From MaRDI portal
Publication:2252530
DOI10.1016/j.ic.2014.02.005zbMath1291.03011arXivmath/0411227OpenAlexW2000644799MaRDI QIDQ2252530
Pietro Ursino, Domenico Cantone
Publication date: 18 July 2014
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/math/0411227
satisfiability problemdecision problemcomputable set theoryfiniteness predicatequantifier-free fragment of set theory MLSSPFsatisfaction algorithmsmall witness-model property
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30)
Related Items
Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*
Uses Software
Cites Work
- 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
- Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators
- The Bernays-Schönfinkel-Ramsey class for set theory: decidability
- The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability
- The Logically Simplest Form of the Infinity Axiom
- Set Theory
- Computational Logic and Set Theory
- Verification: Theory and Practice