Polynomial Constraints For Sets With Cardinality Bounds
FOSSACS'07: Proceedings of the 10th international conference on Foundations of software science and computational structures(2007)
摘要
Logics that can reason about sets and their cardinality bounds are useful in program analysis, program verification, databases, and knowledge bases. This paper presents a class of constraints on sets and their cardinalities for which the satisfiability and the entailment problems are computable in polynomial time. Our class of constraints, based on tree-shaped formulas, is unique in being simultaneously tractable and able to express 1) that a set is a union of other sets, 2) that sets are disjoint, and 3) that a set has cardinality within a given range. As the main result we present a polynomial-time algorithm for checking entailment of our constraints.
更多查看译文
关键词
cardinality bound,entailment problem,program analysis,program verification,knowledge base,main result,polynomial time,polynomial-time algorithm,tree-shaped formula,polynomial constraint
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要