Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate

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

zbMATH Keywords

satisfiability problemdecision problemcomputable set theoryfiniteness predicatequantifier-free fragment of set theory MLSSPFsatisfaction algorithmsmall witness-model property

Mathematics Subject Classification ID

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

• AEtnaNova
• Referee

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