Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator

DOI10.1016/0022-0000(87)90001-8zbMath0634.03008OpenAlexW2026242340MaRDI QIDQ1096608

Alfredo Ferro, Domenico Cantone

Publication date: 1987

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(87)90001-8

zbMATH Keywords

algorithmsatisfiability of quantifier free formulas

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Foundations of classical theories (including reverse mathematics) (03B30) Set theory (03E99)

Related Items (2)

The automation of syllogistic. I: Syllogistic normal forms ⋮ A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions

Cites Work

• Unnamed Item
• Unnamed Item
• Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
• Another proof of E. Hopf's ergodic lemma
• Decision procedures for elementary sublanguages of set theory. IV. Formulae involving a rank operator or one occurrence of Σ(x)={{y}|y εx}
• Decision algorithms for some fragments of analysis and related areas
• 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

This page was built for publication: Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator