Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae

DOI10.1002/CPA.3160410107zbMATH Open0645.03007OpenAlexW1994793938MaRDI QIDQ3787974FDOQ3787974

Authors: Domenico Cantone, Alfredo Ferro, Eugenio Omodeo 

Publication date: 1988

Published in: Communications on Pure and Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/cpa.3160410107

Recommendations

• Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability
• Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators
• Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
• Decision procedures for elementary sublanguages of set theory. VI. Multi-level syllogistic extended by the powerset operator
• Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator

zbMATH Keywords

interpretationfinite modelsemidecision procedure for finite satisfiability of safe formulasunquantified formulas

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Set theory (03E99)

Cited In (18)

• The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability
• Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate
• A calculus for finitely satisfiable formulas with identity
• Truth In V for ∃*∀∀-Sentences is Decidable
• A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case
• The automation of syllogistic. I: Syllogistic normal forms
• Complete Axiomatisations of Properties of Finite Sets
• A finite analog to the Löwenheim-Skolem theorem
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Title not available (Why is that?)
• A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets
• Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators
• A decision procedure for sets, binary relations and partial functions
• Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
• Decision procedures for elementary sublanguages of set theory IX. Unsolvability of the decision problem for a restricted subclass of the Δ0-formulas in set theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Decision procedures for elementary sublanguages of set theory VII. Validity in set theory when a choice operator is present

This page was built for publication: Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3787974)