A Complete Gentzen-Style Axiomatization for Set Constraints.

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 Φ ⊢ Ψ, where Φ and Ψ are finite sets of set constraints, based on the axioms of termset algebra. Sequents of the restricted form Φ ⊢ ⊥ correspond to positive set constraints, and those of the more general form Φ ⊢ Ψ correspond to systems of mixed positive and negative set constraints. We show that the deductive system is (i) complete for the restricted sequents Φ ⊢ ⊥ over standard models, (ii) incomplete for general sequents Φ ⊢ Ψ over standard models, but (iii) complete for general sequents over set-theoretic termset algebras.KeywordsNormal FormPartial FunctionDeductive SystemPositive SystemDerivation TreeThese keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.