Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal



Hoare logic isn't the right solution for proving that example.  You should
use natural deduction.

Chapter 1 of Logic In Computer Science Michael Huth and Mark Ryan
ISBN 978-0-521-54310-1 will show you how to do this from first principles.
On Apr 24, 2015 11:32 AM, "Mandy Martin" <tesleft at hotmail.com> wrote:

> Hi ,
>
> if want to prove  a simple  logic  such as   a ^  b  v  c  ->  a v  b  ^ c
>
> how to write this  goal  in  terms  of  hoare logic,   {P}  C  {Q}  ?
>
> backward  can  generate  subgoal,  can  forward  generate  subgoal?
>
> is  there  a  Isabelle  script  to show  this  simple  example?
>
> Regards,
>
> Martin Lee
>
> > Date: Thu, 23 Apr 2015 20:36:58 +0800
> > From: heb1001 at gmail.com
> > To: tesleft at hotmail.com
> > CC: cl-isabelle-users at lists.cam.ac.uk
> > Subject: Re: [isabelle] Is there example to use Backward Hoare and
> Forward Floyd to find subgoal from goal
> >
> > I found Chapter 12 of Concrete Semantics [1] and the paper Forward With
> > Hoare [2] useful.
> >
> > [1] http://www.concrete-semantics.org/
> > [2] http://www.cl.cam.ac.uk/~mjcg/Hoare75/paper.pdf
> > On Apr 23, 2015 5:46 PM, "Mandy Martin" <tesleft at hotmail.com> wrote:
> >
> > > Hi sir,
> > > Is there example to use Backward Hoare and Forward Floyd to find
> subgoal
> > > from goal?
> > >
> > > Regards,
> > > Martin Lee
>



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