Theta-Subsumption Ordering

When searching the hypothesis space of clauses, one possible feasible way to quasi-order the hypothesis space is to use θ-subsumption. The general idea is to structure the search space with respect to generality of instances. Intuitively the following definition of "more general than" is reasonable: If c and c' are clauses and c ⊨ c' then c is more general than c'.

However, it is more feasible to define the "more general than"-relation by restricting inference to θ-subsumption. Let C₁ and C₂ be clauses. Then C₁ is more general than C₂, if and only if:
There is a substitution θ, such that C₁θ ⊆ C₂ .