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”.
Domenico Aldo Cantone, Jacob T. Schwartz, Calogero G. Zarba · Electronic Notes in Theoretical Computer Science · 2003
MLSS is a decidable sublanguage of set theory involving the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton. In this paper we extend MLSS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We prove that the resulting language is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of MLSS.