Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
type: Item
instance of: scholarly article
title: Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
zbMATH Open document ID: 0634.03008
DOI: 10.1016/0022-0000(87)90001-8
published in: Journal of Computer and System Sciences
publication date: 1987-01-01T00:00:00Z
review text: [For Part IV see Commun. Pure Appl. Math. 40, 37-77 (1987; Zbl 0595.03007).] Quantifier free formulas are Boolean combinations of the following atomic expressions: \(x=y\cup z\), \(x=y\setminus z\), \(x\in y\), \(x=\emptyset\), \(u=Un(y)\) (here \(u=Un(y)\) is intended to mean the set u is the union of the set y). A standard interpretation for a quantifier free formula is a function which assigns to every variable x a set Mx. A set of quantifier free formulas is satisfiable if there is some (standard) interpretation which makes all the formulas in the set true. In this paper an algorithm is presented for deciding the satisfiability of quantifier free formulas.
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03E99
Mathematics Subject Classification ID: 03B30
zbMATH DE Number: 4031632
zbMATH Keywords: algorithm
zbMATH Keywords: satisfiability of quantifier free formulas
author: Domenico Cantone
author: Alfredo Ferro
author: Jacob T. Schwartz
reviewed by: J. M. Plotkin
MaRDI profile type: Publication
full work available at URL: 0022-0000(87)90001-8
OpenAlex ID: W2026242340
cites work: Another proof of E. Hopf's ergodic lemma
cites work: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
cites work: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
cites work: 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: Decision procedures for elementary sublanguages of set theory. IV. Formulae involving a rank operator or one occurrence of Σ(x)={{y}|y εx}
cites work: Decision algorithms for some fragments of analysis and related areas
cites work: Q4091421
cites work: Q3852172
description: scientific article; zbMATH DE number 4031632