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

```I know how to prove resolution

But it is proved by contradiction,

I interested in its subgoal which is about the algorithm in the way of proving

I have another question is how to use resolution with lift
I do not understand "with lift"

> Date: Fri, 24 Apr 2015 13:29:07 +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
>
> 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
> >
```

• Follow-Ups:
• References:

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