*To*: Harry Butterworth <heb1001 at gmail.com>*Subject*: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Fri, 24 Apr 2015 10:27:14 +0100*Cc*: Mandy Martin <tesleft at hotmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMUwPhw9SMPjihTvvXxcrWpPGht41LR7WTo3BupwP44ZJMr9NA@mail.gmail.com>*References*: <BAY167-W17FEC3D9F0BFF25311A957B6ED0@phx.gbl> <CAMUwPhw+ZBgCGnfqFKEb0Q0+LoBNPAWgtGyzAC3Zqzmp+KHKug@mail.gmail.com> <BAY167-W3491452282B2834DC91DF6B6EC0@phx.gbl> <CAMUwPhzshcGE6VomkB_6xX2vex__L85jnxrVXONEqwno+s=Rbg@mail.gmail.com> <BAY167-W9351F8B2543C7355E76DBB6EC0@phx.gbl> <CAMUwPhw9SMPjihTvvXxcrWpPGht41LR7WTo3BupwP44ZJMr9NA@mail.gmail.com>

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**:**[isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal***From:*Mandy Martin

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

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

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

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

- Previous by Date: Re: [isabelle] libisabelle: Small Scala library to communicate with Isabelle
- Next by Date: Re: [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach
- Previous by Thread: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- Next by Thread: [isabelle] Division-ring for fields
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list