Publication Details
Title: Decision Procedures for Flat Set-Theorectical Syllogistics.I. General Union, Powerset and Singleton Operators
Author: D. Cantone and V. Cutello
Group: ICSI Technical Reports
Date: May 1992
PDF: http://www.icsi.berkeley.edu/pubs/techreports/TR-92-031.pdf
Overview:
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.
Bibliographic Information:
ICSI Technical Report TR-92-031
Bibliographic Reference:
D. Cantone and V. Cutello. Decision Procedures for Flat Set-Theorectical Syllogistics.I. General Union, Powerset and Singleton Operators. ICSI Technical Report TR-92-031, May 1992
Author: D. Cantone and V. Cutello
Group: ICSI Technical Reports
Date: May 1992
PDF: http://www.icsi.berkeley.edu/pubs/techreports/TR-92-031.pdf
Overview:
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.
Bibliographic Information:
ICSI Technical Report TR-92-031
Bibliographic Reference:
D. Cantone and V. Cutello. Decision Procedures for Flat Set-Theorectical Syllogistics.I. General Union, Powerset and Singleton Operators. ICSI Technical Report TR-92-031, May 1992