کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426755 | 686259 | 2014 | 28 صفحه PDF | دانلود رایگان |
In this paper we solve the satisfiability problem for the quantifier-free fragment of set theory MLSSPF involving in addition to the basic Boolean set operators of union, intersection, and difference, also the powerset and singleton operators, and a finiteness predicate.The more restricted fragment obtained by dropping the finiteness predicate has been shown to have a solvable satisfiability problem in a previous paper, by establishing for it a small model property.We exploit the latter decision result for dealing also with the finiteness predicate (and therefore with the infiniteness predicate too) and prove a small witness-model property for MLSSPF, asserting that any model for a satisfiable formula Φ with m distinct variables of the fragment of our interest admits a finite representation bounded by c(m)c(m), where c is a suitable computable function. Since such candidate representations are finitely many, their number does not exceed a known bound, and it can be recognized algorithmically whether they indeed represent a(n infinite) model for the input formula, the decidability of the satisfiability problem for MLSSPF follows.
Journal: Information and Computation - Volume 237, October 2014, Pages 215–242