(sorry. I just sent the previous email by mistake, here is the complete
version)
Dear all,
I wonder if there is better way to handle proofs like (((A==>B)==> C)==>
D)==> E (in top-down proofs, I also wonder how I should do it in bottom up
proofs),
After doing a UNDISCH, all the A...D will go to the hypothesis part. I
understand that in natural deduction, we don't do much on the hypothesis
side. So apart from doing MP to get:
K ==> (((A==>B)==> C)==> D)==> E K
---------------------------------------------------------- MP
(((A==>B)==> C)==> D)==> E
and EQ_MP (which is similar as above), what else could I do to make a less
painful proof?
Sorry again for sending the previous email a few sec ago unexpectedly.
Thanks very much.
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
