(14th-August-2020)
• The bottom-up implementation is an augmented version of the bottom-up algorithm for definite clauses presented in Section 5.2.2.1.
• The modification to that algorithm is that the conclusions are pairs ⟨a,A⟩, where a is an atom and A is a set of assumables that imply a in the context of Horn clause knowledge base KB.
• Initially, the conclusion set C is {⟨a,{a}⟩:a is assumable}. Clauses can be used to derive new conclusions. If there is a clause h←b1∧...∧bm such that for each bi there is some Ai such that ⟨bi,Ai⟩ ∈C, then ⟨h,A1∪...∪Am⟩ can be added to C. Note that this covers the case of atomic clauses, with m=0, where ⟨h,{}⟩ is added to C.
Comments