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

```I assume that this is a reference to lifting, which is a technical aspect of how resolution works in Isabelle. It is described in an early paper of mine, see below. But this is definitely not a user's question; it is only relevant from a theoretical point of view or for somebody wanting to build an analogous theorem prover.

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.html

Larry Paulson

> On 24 Apr 2015, at 09:08, Harry Butterworth <heb1001 at gmail.com> wrote:
>
> 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
>>>>
>>
>

```

• References:

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