Skip to Main content Skip to Navigation
Reports

A Decision Procedure for a Fragment of Set Theory Involving Monotone, Additive, and Multiplicative Functions

Calogero G. Zarba 1 Domenico Cantone Jacob T. Schwartz
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this report we extend 2LS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We call the resulting language 2LSmf. We prove that 2LSmf is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of 2LS. Furthermore, we prove that the language 2LSmf is stably infinite with respect to the sort of elements. Therefore, using a many-sorted version of the Nelson-Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00070731
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 9:27:21 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:14:26 PM

Identifiers

  • HAL Id : inria-00070731, version 1

Citation

Calogero G. Zarba, Domenico Cantone, Jacob T. Schwartz. A Decision Procedure for a Fragment of Set Theory Involving Monotone, Additive, and Multiplicative Functions. [Research Report] RR-5267, INRIA. 2004, pp.22. ⟨inria-00070731⟩

Share

Metrics

Record views

225

Files downloads

253