CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIn 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 Phi with m distinct variables of the fragment of our interest admits a finite representation bounded by 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.
| Titolo: | Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, finiteness predicate | |
| Autori interni: | ||
| Data di pubblicazione: | 2014 | |
| Rivista: | ||
| Handle: | http://hdl.handle.net/20.500.11769/16602 | |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
http://hdl.handle.net/20.500.11769/16602
Copyright © 2022