Decision Procedures for Flat Set-Theorectical Syllogistics.I. General Union, Powerset and Singleton Operators

TitleDecision Procedures for Flat Set-Theorectical Syllogistics.I. General Union, Powerset and Singleton Operators
Publication TypeTechnical Report
Year of Publication1992
AuthorsCantone, D., & Cutello V.
Other Numbers736
Abstract

In this paper we show that a class of unquantified multi-sorted set-theoretic formulae involving the notions of powerset, general union, and singleton has a solvable satisfiability problem. We exhibit a normalization procedure that given a model for a formula in our theory, it produces a simpler and "a priori" bounded model whose cardinality depends solely on the size of the given formula.

URLhttp://www.icsi.berkeley.edu/pubs/techreports/TR-92-031.pdf
Bibliographic Notes

ICSI Technical Report TR-92-031

Abbreviated Authors

D. Cantone and V. Cutello

ICSI Publication Type

Technical Report