On Wed, Jul 11, 2012 at 8:38 PM, "Mark" <m...@proof-technologies.com> wrote:
> I intend to cater for both the declarative style (i.e. stating the result
> of
> the step) and the imperative style (i.e. stating what operation to apply
> next), and a mixture of both. I think that this is a huge subject that has
> not been properly explored yet by existing systems.
I would say one can write proof scripts in a mixture of imperative and
declarative styles already in HOL4, in particular using things like "by",
"TRY", and the various matching, renaming, and abbreviating tactics for the
declarative parts. It's a matter of self-discipline how much you want to
explicitly state formulae you're proving or manipulating. Is there
something more to declarative proofs that I'm missing?
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
