Editing Inductive logic programming (section)

=== Bottom-up search ===
Bottom-up methods to search the subsumption lattice have been investigated since Plotkin's first work on formalising induction in clausal logic in 1970.<ref name=":02"/><ref>{{cite thesis |first=G.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}}</ref> Techniques used include least general generalisation, based on [[Anti-unification (computer science)|anti-unification]], and inverse resolution, based on inverting the [[Resolution (logic)|resolution]] inference rule.

==== Least general generalisation ====
A ''least general generalisation algorithm'' takes as input two clauses <math display="inline">C_1</math> and <math display="inline">C_2</math> and outputs the least general generalisation of  <math display="inline">C_1</math> and <math display="inline">C_2</math>, that is, a clause  <math display="inline">C</math> that subsumes  <math display="inline">C_1</math> and <math display="inline">C_2</math>, and that is subsumed by every other clause that subsumes  <math display="inline">C_1</math> and <math display="inline">C_2</math>. The least general generalisation can be computed by first computing all ''selections'' from <math display="inline">C</math> and <math display="inline">D</math>, which are pairs of literals  <math>(L,M) \in (C_1, C_2)</math> sharing the same predicate symbol and negated/unnegated status.  Then, the least general generalisation is obtained as the disjunction of the least general generalisations of the individual selections, which can be obtained by [[first-order syntactical anti-unification]].<ref>{{Cite book |last1=Nienhuys-Cheng |first1=Shan-hwei |title=Foundations of inductive logic programming |last2=Wolf |first2=Ronald de |date=1997 |publisher=Springer |isbn=978-3-540-62927-6 |series=Lecture notes in computer science Lecture notes in artificial intelligence |location=Berlin Heidelberg |page=255}}</ref>

To account for background knowledge, inductive logic programming systems employ ''relative least general generalisations'', which are defined in terms of subsumption relative to a background theory. In general, such relative least general generalisations are not guaranteed to exist; however, if the background theory ''{{mvar|B}}'' is a finite set of [[Ground expression|ground]] [[Literal (mathematical logic)|literals]], then the negation of ''{{mvar|B}}'' is itself a clause. In this case, a relative least general generalisation can be computed by disjoining the negation of ''{{mvar|B}}'' with both <math display="inline">C_1</math> and <math display="inline">C_2</math> and then computing their least general generalisation as before.<ref>{{Cite book |last1=Nienhuys-Cheng |first1=Shan-hwei |title=Foundations of inductive logic programming |last2=Wolf |first2=Ronald de |date=1997 |publisher=Springer |isbn=978-3-540-62927-6 |series=Lecture notes in computer science Lecture notes in artificial intelligence |location=Berlin Heidelberg |page=286}}</ref>

Relative least general generalisations are the foundation of the bottom-up system [[Golem (ILP)|Golem]].<ref name=":12"/><ref name="Springer/Ohmsha"/>

==== Inverse resolution ====
Inverse resolution is an [[inductive reasoning]] technique that involves [[wiktionary:invert|inverting]] the [[Resolution (logic)|resolution operator]].

Inverse resolution takes information about the [[Resolvent (logic)|resolvent]] of a resolution step to compute possible resolving clauses. Two types of inverse resolution operator are in use in inductive logic programming: V-operators and W-operators. A V-operator takes clauses <math display="inline">R</math> and <math display="inline">C_1</math>as input and returns a clause <math display="inline">C_2</math> such that <math display="inline">R</math> is the resolvent of <math display="inline">C_1</math> and  <math display="inline">C_2</math>. A W-operator takes two clauses <math display="inline">R_1</math> and <math display="inline">R_2</math> and returns three clauses <math display="inline">C_1</math>, <math display="inline">C_2</math> and <math display="inline">C_3</math> such that <math display="inline">R_1</math> is the resolvent of <math display="inline">C_1</math> and <math display="inline">C_2</math> and <math display="inline">R_2</math> is the resolvent of  <math display="inline">C_2</math> and <math display="inline">C_3</math>.<ref name="invres">{{Cite book |last1=Nienhuys-Cheng |first1=Shan-hwei |title=Foundations of inductive logic programming |last2=Wolf |first2=Ronald de |date=1997 |publisher=Springer |isbn=978-3-540-62927-6 |series=Lecture notes in computer science Lecture notes in artificial intelligence |location=Berlin Heidelberg |page=197}}</ref>

Inverse resolution was first introduced by [[Stephen Muggleton]] and Wray Buntine in 1988 for use in the inductive logic programming system Cigol.<ref name="Proceedings of the 5th Internationa"/> By 1993, this spawned a surge of research into inverse resolution operators and their properties.<ref name="invres" />