Instance-Based Theorem Proving

Moderator: Automated Theorem Proving

LordHoto
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 135
Registriert: 14. Dez 2009 17:00

Instance-Based Theorem Proving

Beitrag von LordHoto » 2. Aug 2014 20:41

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
Compiler 1 Tutor WS 12/13

aeflores
Moderator
Moderator
Beiträge: 5
Registriert: 4. Apr 2013 14:58

Re: Instance-Based Theorem Proving

Beitrag von aeflores » 4. Aug 2014 16:56

hi Johannes,
You are right, there was a mistake in the slides. I just uploaded a corrected version to the course webpage.
Antonio

Antworten

Zurück zu „Automated Theorem Proving“