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

```Is your first language Chinese?  If so, you can send me a more
detailed question in simplified Chinese in a private email.  As a
minimum, you're going to have to include more context about the "with
lift" part.  I can work with one of my Chinese colleagues here to try
to point you in the right direction.

On 24/04/2015, Mandy Martin <tesleft at hotmail.com> wrote:
> 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.