PS: What about a function that supports backward-chaining with Z theorems, something like z_bc_tac and z_bc_thm_tac? I suppose this could be quite useful too. Is there anything more that needs to be done other than rewriting the Z universal quantifier into a HOL one, and using the HOL backward-chaining tactics?Yes. I have been meaning to get round to this for a long time. It isn't quite as simple as you might think because the Z tactics are designed to keep in Z, but the back-chaining tactics often need to produce an existentially quantified goal and that would need to be converted from HOL back into Z.
I was often finding that I wanted to backward-chain in Z so I wrote a simple version of z_bc_thm_tac as attached. It may not do everything that is required of such a tactic and doesn't have any proper error management but it has been sufficient for my purposes.
PhilThe information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order.
For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful.
Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this.
Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes.
QinetiQ Limited Registered in England & Wales: Company Number:3796233 Registered office: 85 Buckingham Gate, London SW1E 6PD, United KingdomTrading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://www.qinetiq.com/home/notices/legal.html
z_bc_thm_tac.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
