A Complete Gentzen-style Axiomatization for Set Constraints

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.