Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
From MaRDI portal
Publication:3916545
DOI10.1002/cpa.3160340203zbMath0465.03003OpenAlexW2101118111MaRDI QIDQ3916545
Alfredo Ferro, Michael Breban, Eugenio Giovanni Omodeo
Publication date: 1981
Published in: Communications on Pure and Applied Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1002/cpa.3160340203
mappingsalgorithmordinalsbounded existential quantifiersbounded universal quantifiersformulas in prenex normal formsatisfiability problem for quantifier free formulas
Related Items (11)
Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator ⋮ Decidability and completeness for open formulas of membership theories ⋮ The Logically Simplest Form of the Infinity Axiom ⋮ The automation of syllogistic. I: Syllogistic normal forms ⋮ Set-syllogistics meet combinatorics ⋮ A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case* ⋮ The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability ⋮ Goals and benchmarks for automated map reasoning ⋮ The automation of syllogistic. II: Optimization and complexity issues ⋮ Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
Cites Work
This page was built for publication: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
