on 10/7/12 4:50 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> Mark, since this is an HOL newsgroup, can you say something about how > you're going to do this? Why is your classic "LCF-style" interactive > theorem prover going to be better than HOL Light & miz3, which is not > suitable yet for such quick and trivial formalising? Above the low level stuff (the inference kernel, the parser/printer, the derivation of its low-level inference rules), it will be implemented in a completely different way to the existing systems. I don't expect anyone to believe me in how effective it will be until I've actually implemented it and > I thought a little about why I mean by the "trivial" stuff I want the > proof assistant to do. Perhaps this is exactly what miz3 does. > Suppose I have a line > > STATEMENT by R1, R2, ..., Rn; > > miz3 ought to check this, I hazily imagine, by: ... > > Perhaps a more rudimentary proof assistant ought to require the user > to specify how to substitute our defined variables for the free > variables in the theorems. .... 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. Mark. ------------------------------------------------------------------------------ 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
