Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. A Complete Gentzen-style Axiomatization for Set Constraints

A Complete Gentzen-style Axiomatization for Set Constraints

File(s)
95-1518.ps (210.1 KB)
95-1518.pdf (238.77 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7175
Collections
Computer Science Technical Reports
Author
Cheng, Allan
Kozen, Dexter
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.

Date Issued
1995-05
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1518
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance