Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Inclusion Constraints over Non-Empty Sets of Trees

Martin Müller, Joachim Niehren, Andreas Podelski

Theory and Practice of Software Development, International Joint Conference CAAP/FASE/TOOLS, Vol. 1214 of LNCS, pp. 217-231, springer, April 1997

We present a new constraint system called Ines. Its constraints are conjunctions of inclusions $t_1subseteq t_2$ between first-order terms (without set operators) which are interpreted over non-empty sets of trees. The existing systems of set constraints can express Ines constraints only if they include negation. Their satisfiability problem is NEXPTIME-complete. We present an incremental algorithm that solves the satisfiability problem of Ines constraints in cubic time. We intend to apply Ines constraints for type analysis for a concurrent constraint programming language.

Download PDF        Show BibTeX               

@INPROCEEDINGS{ines97,
  title = {Inclusion Constraints over Non-Empty Sets of Trees},
  author = {Martin Müller and Joachim Niehren and Andreas Podelski},
  year = {1997},
  month = {apr},
  editor = {{Max Dauchet}},
  publisher = {springer},
  booktitle = {Theory and Practice of Software Development, International Joint Conference CAAP/FASE/TOOLS},
  series = {LNCS},
  volume = {{1214}},
  pages = {{217-231}},
}

Login to edit