A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case

DOI10.1007/S10817-004-6243-3zbMath1067.03019OpenAlexW2087368574MaRDI QIDQ556680

Domenico Cantone, Calogero G. Zarba

Publication date: 22 June 2005

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-004-6243-3

zbMATH Keywords

set theorydecision procedureNelson-Oppen procedure

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30)

Uses Software

• SETL

Cites Work

• Simplification by Cooperating Decision Procedures
• Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
• The B-Book
• 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”.
• Verification: Theory and Practice
• Logics in Artificial Intelligence
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case