Re: [isabelle] Elim resolution



The removal of an assumption indeed sounds like we are getting something for nothing. However, remember that we use backward proof; removal of an assumption actually means you have to prove the subgoal With fewer facts than you were entitled to use. The reason it is beneficial to remove this assumption is simply that it will be redundant.
Larry Paulson


On 12 Jan 2009, at 01:19, Chris Capel wrote:

I follow up to this point. Here the book skips right to [| P ==> P; P
==> P |] ==> P | P --> P. I understand how it was unified, and I
understand how the first subgoal, "P | P ==> ?Q | ?R" before
unification, was discharged automatically as part of elim resolution,
but I don't understand how the first assumption "P | P" from the two
remaining subgoals can be eliminated. How is that justified?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.