scientific article; zbMATH DE number 1507186

MaRDI QIDQ4503906zbMATH OpenFDO

Authors Domenico Cantone, Calogero G. Zarba

Publication date 14 September 2000

zbMATH Keywords

Multi-Level Syllogistic with Singletontableau-based decision procedure

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Recommendations

• scientific article; zbMATH DE number 1341470
• A tableau-based decision procedure for a fragment of set theory with iterated membership
• scientific article; zbMATH DE number 1612563
• A fast saturation strategy for set-theoretic tableaux
• Publication:4867922
• A tableaux-based theorem prover for a decidable subset of default logic
• scientific article; zbMATH DE number 1189098
• Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae
• Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus
• A more efficient tableaux procedure for simultaneous search for refutations and finite models

Cited in

(15)

• Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators
• Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership
• scientific article; zbMATH DE number 1612563 (Why is no real title available?)
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• scientific article; zbMATH DE number 5898609 (Why is no real title available?)
• Semantics of admissible sets of truth values for S5. The decision procedure
• Satisfiability modulo theories
• scientific article; zbMATH DE number 1189098 (Why is no real title available?)
• scientific article; zbMATH DE number 1341470 (Why is no real title available?)
• Reasoning with finite sets and cardinality constraints in SMT
• A fast saturation strategy for set-theoretic tableaux
• scientific article; zbMATH DE number 851448 (Why is no real title available?)
• Complexity assessments for decidable fragments of set theory. I: A taxonomy for the Boolean case
• Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
• A tableau-based decision procedure for a fragment of set theory with iterated membership

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4503906)