Instance-Based Theorem Proving
I have a question about slide 19 (54/59) of the lecture on IBTP. The last condition in the definition "Inst-Gen Rule with Ground Closure" does not make any sense to me. Shouldn't it rather list sigma applied to the second clause premise on the LHS of the equation? Or maybe someone can explain to me what this is about.