Theta-subsumption
Theta-subsumption is a decidable relation between two first-order clauses that guarantees that one clause logically entails the other. It was first introduced by John Alan Robinson in 1965 and has become a fundamental notion in inductive logic programming. Deciding whether a given clause θ-subsumes another is an NP-complete problem.
Definition
A clause, that is, a disjunction of first-order literals, can be considered as a set containing all its disjuncts.With this convention, a clause θ-subsumes a clause if there is a substitution such that the clause obtained by applying to is a subset of.
Properties
θ-subsumption is a weaker relation than logical entailment, that is, whenever a clause θ-subsumes a clause , then logically entails. However, the converse is not true: A clause can logically entail another clause, but not θ-subsume it.θ-subsumption is decidable; more precisely, the problem of whether one clause θ-subsumes another is NP-complete in the length of the clauses. This is still true when restricting the setting to pairs of Horn clauses.
As a binary relation among Horn clauses, θ-subsumption is reflexive and transitive. It therefore defines a preorder. It is not antisymmetric, since different clauses can be syntactic variants of each other. However, in every equivalence class of clauses that mutually θ-subsume each other, there is a unique shortest clause up to variable renaming, which can be effectively computed. The class of quotients with respect to this equivalence relation is a complete lattice, which has both infinite ascending and infinite descending chains. A subset of this lattice is known as a.