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 θ-subsumes a clause if there is a substitution such that the clause obtained by applying to is a subset of .[1]

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.[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. ^ a b De Raedt 2008, p. 127.
  2. ^ a b c Kietz & Lübbe 1994.
  3. ^ De Raedt 2008, pp. 131–135.
  4. ^ Robinson 1965.
  5. ^ Plotkin 1970, p. 39.
  6. ^ Baxter 1977.
  7. ^ 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, 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.