Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions

DOI10.1002/cpa.3160330503zbMath0453.03009OpenAlexW2095098901WikidataQ56061184 ScholiaQ56061184MaRDI QIDQ3900014

Alfredo Ferro, Jacob T. Schwartz, Eugenio Giovanni Omodeo

Publication date: 1980

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

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

zbMATH Keywords

first order set theoretic languagesatisfiability of quantifier free formulas

Mathematics Subject Classification ID

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

Related Items

Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator, The automation of syllogistic. I: Syllogistic normal forms, A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions1 1This research has been partially supported by MURST Grant prot. 2001017741 under project “Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche”., First steps towards exact algebraic identification, Set-syllogistics meet combinatorics, Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages, A fast saturation strategy for set-theoretic tableaux, Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership, A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions, Une procédure de décision pour un problème de satisfiabilité dans un univers ensembliste héréditairement fini, Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*, Goals and benchmarks for automated map reasoning, A system of relational syllogistic incorporating full Boolean reasoning, A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case, Unnamed Item, THE LOGIC OF COMPARATIVE CARDINALITY, Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator, Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets, A tableau-based decision procedure for a fragment of set theory with iterated membership, Combining sets with cardinals