*To*: <heb1001 at gmail.com>*Subject*: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal*From*: Mandy Martin <tesleft at hotmail.com>*Date*: Fri, 24 Apr 2015 14:29:32 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*Importance*: Normal*In-reply-to*: <CAMUwPhzshcGE6VomkB_6xX2vex__L85jnxrVXONEqwno+s=Rbg@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>

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**:**[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

- Previous by Date: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- Next by Date: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- Previous by Thread: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- Next by Thread: Re: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- 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