Abstract
We extend the unquantified set-theoretic fragment discussed in [1] with a restricted form of quantification, we prove decidability of the resulting fragment by means of a tableau calculus and we address the efficiency problem of the underlying decision procedure, by showing that the model-checking steps used in [1] are not necessary.
Cite
CITATION STYLE
Cantone, D., & Zarba, C. G. (1999). A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 97–112). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
