Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: A Complete Gentzen-style Axiomatization for Set Constraints
Authors: Cheng, Allan
Kozen, Dexter
Keywords: computer science
technical report
Issue Date: May-1995
Publisher: Cornell University
Abstract: Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide a Gentzen-style axiomatization for sequents $\Phi\force\Psi$, where $\Phi$ and $\Psi$ are finite sets of set constraints, based on the axioms of termset algebra. Sequents of the restricted form $\Phi\force\bottom$ correspond to positive set constraints, and those of the more general form $\Phi\force\Psi$ correspond to systems of mixed positive and negative set constraints. We show that the deductive system is (i) complete for the restricted sequents $\Phi\force\bottom$ over standard models, (ii) incomplete for general sequents $\Phi\force\Psi$ over standard models, but (iii) complete for general sequents over set-theoretic termset algebras.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
95-1518.pdf238.77 kBAdobe PDFView/Open
95-1518.ps210.1 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us