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 [math]\displaystyle{ c_1 }[/math] θ-subsumes a clause [math]\displaystyle{ c_2 }[/math] if there is a substitution [math]\displaystyle{ \theta }[/math] such that the clause obtained by applying [math]\displaystyle{ \theta }[/math] to [math]\displaystyle{ c_1 }[/math] is a subset of [math]\displaystyle{ c_2 }[/math].[1]
Properties
θ-subsumption is a weaker relation than logical entailment, that is, whenever a clause [math]\displaystyle{ c_1 }[/math] θ-subsumes a clause [math]\displaystyle{ c_2 }[/math], then [math]\displaystyle{ c_1 }[/math] logically entails [math]\displaystyle{ c_2 }[/math]. 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.[3]
History
θ-subsumption was first introduced by J. Alan Robinson in 1965 in the context of resolution,[4] and was first applied to inductive logic programming by Gordon Plotkin in 1970 for finding and reducing least general generalisations of sets of clauses.[5] In 1977, Lewis D. Baxter proves that θ-subsumption is NP-complete,[6] and the 1979 seminal work on NP-complete problems, Computers and Intractability, includes it among its list of NP-complete problems.[2]
Applications
Theorem provers based on the resolution or superposition calculus use θ-subsumption to prune redundant clauses.[7] 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.[1] It is further used to test whether a clause covers an example, and to determine whether a given pair of clauses is redundant.[2]
Notes
- ↑ 1.0 1.1 De Raedt 2008, p. 127.
- ↑ 2.0 2.1 2.2 Kietz & Lübbe 1994.
- ↑ De Raedt 2008, pp. 131–135.
- ↑ Robinson 1965.
- ↑ Plotkin 1970, p. 39.
- ↑ Baxter 1977.
- ↑ Waldmann et al. 2022.
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, doi:10.1007/978-3-540-68856-3, ISBN 978-3-540-20040-6, Bibcode: 2008lrl..book.....D, http://dx.doi.org/10.1007/978-3-540-68856-3
- 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, http://dx.doi.org/10.1016/b978-1-55860-335-6.50024-6, 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.
- Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin (November 2022). "A Comprehensive Framework for Saturation Theorem Proving" (in en). Journal of Automated Reasoning 66 (4): 499–539. doi:10.1007/s10817-022-09621-7. ISSN 0168-7433. PMID 36353684.
 |  |
