2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper 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, by using a many-sorted version of the Nelson-Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.

A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case

CANTONE, Domenico;
2004-01-01

Abstract

2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper 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, by using a many-sorted version of the Nelson-Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.
set theory; decision procedure; Nelson-Oppen procedure
File in questo prodotto:
File Dimensione Formato  
ZarbaCantoneSchwartz-JAR2004.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Dimensione 254.39 kB
Formato Adobe PDF
254.39 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11769/49305
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact