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 $c_1$ θ-subsumes a clause $c_2$ if there is a substitution $\theta$ such that the clause obtained by applying $\theta$ to $c_1$ is a subset of $c_2$ .{{sfn|De Raedt|2008|p=127}}

Properties

θ-subsumption is a weaker relation than logical entailment, that is, whenever a clause $c_1$ θ-subsumes a clause $c_2$ , then $c_1$ logically entails $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.{{sfn|Kietz|Lübbe|1994}}

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 {{Visible anchor|refinement graph|text=refinement graph}}.{{Sfn|De Raedt|2008|pp=131–135}}

History

θ-subsumption was first introduced by J. Alan Robinson in 1965 in the context of resolution,{{sfn|Robinson|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.{{sfn|Plotkin|1970|p=39}} In 1977, Lewis D. Baxter proves that θ-subsumption is NP-complete,{{sfn|Baxter|1977}} and the 1979 seminal work on NP-complete problems, Computers and Intractability, includes it among its list of NP-complete problems.{{sfn|Kietz|Lübbe|1994}}

Applications

Theorem provers based on the resolution or superposition calculus use θ-subsumption to prune redundant clauses.{{sfn|Waldmann|Tourret|Robillard|Blanchette|2022}} 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.{{Sfn|De Raedt|2008|p=127}} It is further used to test whether a clause covers an example, and to determine whether a given pair of clauses is redundant.{{sfn|Kietz|Lübbe|1994}}

Notes

References

{{Cite thesis |last=Baxter |first=Lewis Denver |title=The complexity of unification |date=September 1977 |publisher=University of Waterloo |url=https://cs.uwaterloo.ca/research/tr/1977/CS-77-25.pdf}}
{{Citation |last=De Raedt |first=Luc |editor-first1= |editor-last1= |url=http://dx.doi.org/10.1007/978-3-540-68856-3 |title=Logical and Relational Learning |series=Cognitive Technologies |place=Berlin, Heidelberg |publisher=Springer |year=2008 |doi=10.1007/978-3-540-68856-3 |bibcode=2008lrl..book.....D |isbn=978-3-540-20040-6|url-access=subscription }}
{{Citation |last1=Kietz |first1=Jörg-Uwe |title=An Efficient Subsumption Algorithm for Inductive Logic Programming |date=1994 |url=http://dx.doi.org/10.1016/b978-1-55860-335-6.50024-6 |work=Machine Learning Proceedings 1994 |pages=130–138 |access-date=2023-11-26 |publisher=Elsevier |last2=Lübbe |first2=Marcus|doi=10.1016/b978-1-55860-335-6.50024-6 |isbn=9781558603356 |url-access=subscription }}
{{cite thesis |first=Gordon D. |last=Plotkin |title=Automatic Methods of Inductive Inference |date=1970 |type=PhD |publisher=University of Edinburgh |url=https://www.era.lib.ed.ac.uk/bitstream/handle/1842/6656/Plotkin1972.pdf |hdl=1842/6656}}
{{Cite journal |last=Robinson |first=J. A. |title=A Machine-Oriented Logic Based on the Resolution Principle |date=1965 |journal=Journal of the ACM |pages=23–41|volume=12|issue=1|doi=10.1145/321250.321253 |s2cid=14389185 |doi-access=free }}
{{Cite journal |last1=Waldmann |first1=Uwe |last2=Tourret |first2=Sophie |last3=Robillard |first3=Simon |last4=Blanchette |first4=Jasmin |date=November 2022 |title=A Comprehensive Framework for Saturation Theorem Proving |journal=Journal of Automated Reasoning |language=en |volume=66 |issue=4 |pages=499–539 |doi=10.1007/s10817-022-09621-7 |issn=0168-7433 |pmc=9637109 |pmid=36353684}}

Category:Inductive logic programming

Category:Logical consequence

Category:NP-complete problems