It is an data index to retrieve among a set of formulas the ones which contains (or subsumes) by another formula. Also, the inverse problem can be considered where we look for the formulas in the set that are contained by another one. These problems are respectively call forward and backward containment check.
It is commonly used to maintain a set of formulas "minimal" upon insertions, where "minimal" means that the formulas of the set are pairwise not comparable.
Query containment check
- DBLP:conf/birthday/Schulz13 presents an framework for build an index for forward and backward containment check on clauses build from simple discriminating checks f compatible with the subsumption, i.e. f(C) <= f(C') is necessary for C to subsume C, but this article does not give enough details about which f checks to choose in practice.