A tableau-based decision procedure for a fragment of set theory with iterated membership

DOI10.1007/s10817-004-8271-4zbMath1085.03010OpenAlexW2023230345MaRDI QIDQ812437

Calogero G. Zarba, Rosa Ruggeri Cannata, Domenico Cantone

Publication date: 23 January 2006

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

Full work available at URL: https://doi.org/10.1007/s10817-004-8271-4

zbMATH Keywords

set theorysemantic tableaudecision 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)

Related Items (1)

A fast saturation strategy for set-theoretic tableaux

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The automation of syllogistic. II: Optimization and complexity issues
• Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
• Techniques of computable set theory with applications to proof verification
• Verification: Theory and Practice

This page was built for publication: A tableau-based decision procedure for a fragment of set theory with iterated membership