Hi Robert,
This is more a pure logic answer than a HOL-specific one, but... The reason
why (((A==>B)==> C)==> D)==> E is hard to prove is because it is has a very
awkward interpretation, especially in intuitionistic logic (where I expect
the statement is unprovable unless it trivialises in some way). In
classical logic, since the statement is equivalent to (A \/ C \/ E) /\ (!B
\/ C \/ E) /\ (!D /\ E) in CNF, you could reduce the goal to proving (!A /\
!C) ==> E, (B /\ !C) ==> E, D ==> E which lend themselves more easily to
the usual methods of natural deduction. (I'm no HOL expert, but you could
make the given transformation using TAUT and simplify from there.)
Why are you faced with such an unusual goal shape? Such statements do not
often appear in the course of a larger natural deduction proof.
Mario Carneiro
On Thu, May 21, 2015 at 4:10 PM, Robert White <ai.robert.wangsh...@gmail.com
> wrote:
> (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
>
>
------------------------------------------------------------------------------
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
