Email Gateway (Aug 22 2022 at 09:23): Email Gateway (Aug 22 2022 at 09:23):From: Mandy Martin <tesleft@hotmail.com>
Hi sir,
Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal?
Regards,
Martin Lee
Email Gateway (Aug 22 2022 at 09:23):From: Harry Butterworth <heb1001@gmail.com>
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
Email Gateway (Aug 22 2022 at 09:23):From: Harry Butterworth <heb1001@gmail.com>
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.
Email Gateway (Aug 22 2022 at 09:24):From: Harry Butterworth <heb1001@gmail.com>
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.
Email Gateway (Aug 22 2022 at 09:24):From: Mandy Martin <tesleft@hotmail.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"
Email Gateway (Aug 22 2022 at 09:24):From: Larry Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 25 2024 at 16:19 UTC