Draft:Theta-subsumption

Theta-subsumption (θ-subsumption) is an 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 ${\textstyle c_{1}}$ θ-subsumes a clause ${\textstyle c_{2}}$ if there is a substitution $\theta$ such that the clause obtained by applying ${\textstyle \theta }$ to ${\textstyle c_{1}}$ is a subset of ${\textstyle c_{2}}$.

Properties

θ-subsumption is a weaker relation than logical entailment, that is, whenever a clause ${\textstyle c_{1}}$ θ-subsumes a clause ${\textstyle c_{2}}$, then ${\textstyle c_{1}}$ logically entails ${\textstyle c_{2}}$. 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.[2]

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 refinement graph.

History

θ-subsumption was first introduced by J. Alan Robinson in 1965., and was first applied to inductive logic programming by Gordon Plotkin in 1970 for finding and reducing least general generalisations of sets of clauses. In 1977, Lewis D. Baxter proves that θ-subsumption is NP-complete, and the 1979 seminal work on NP-complete problems, Computers and Intractability, includes it among its list of NP-complete problems.

Applications

θ-subsumption is the most fundamental notion of entailment used in inductive logic programming, where it is used as the fundamental notion to determine whether one clause is a specialisation or a generalisation of another. It is further used to test whether a clause covers an example, and to determine whether a given pair of clauses is redundant.

References

• Baxter, Lewis Denver (September 1977). The complexity of unification (PDF) (Thesis). University of Waterloo.
• Robinson, J. A. (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41.
• Plotkin, Gordon D. (1970). Automatic Methods of Inductive Inference (PDF) (PhD). University of Edinburgh. hdl:1842/6656.
• De Raedt, Luc (2008), Logical and Relational Learning, Berlin, Heidelberg: Springer, ISBN 978-3-540-20040-6
• Kietz, Jörg-Uwe; Lübbe, Marcus (1994), "An Efficient Subsumption Algorithm for Inductive Logic Programming", Machine Learning Proceedings 1994, Elsevier, pp. 130–138, retrieved 2023-11-26