Theta-subsumption

Theta-subsumption (θ-subsumption, or just 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 ${\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.

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 in the context of resolution, 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

Theorem provers based on the resolution or superposition calculus use θ-subsumption to prune redundant clauses. In addition, θ-subsumption is the most prominent notion of entailment used in inductive logic programming, where it is the fundamental tool 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.
• De Raedt, Luc (2008), Logical and Relational Learning, Cognitive Technologies, Berlin, Heidelberg: Springer, Bibcode:2008lrl..book.....D, doi:10.1007/978-3-540-68856-3, 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, doi:10.1016/b978-1-55860-335-6.50024-6, ISBN 9781558603356, retrieved 2023-11-26
• Plotkin, Gordon D. (1970). Automatic Methods of Inductive Inference (PDF) (PhD). University of Edinburgh. hdl:1842/6656.
• Robinson, J. A. (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.
• Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin (November 2022). "A Comprehensive Framework for Saturation Theorem Proving". Journal of Automated Reasoning. 66 (4): 499–539. doi:10.1007/s10817-022-09621-7. ISSN 0168-7433. PMC 9637109. PMID 36353684.