Seite 1 von 1

Instance-Based Theorem Proving

Verfasst: 2. Aug 2014 20:41
von LordHoto
Hello,

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.

Thanks,
Johannes

Re: Instance-Based Theorem Proving

Verfasst: 4. Aug 2014 16:56
von aeflores
hi Johannes,
You are right, there was a mistake in the slides. I just uploaded a corrected version to the course webpage.
Antonio