What I am aiming at is a theorem prover that makes formalising such pen-and-paper [Undergraduate textbook] proofs quick and trivial.
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? 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: Some of the reasons Ri are labels of statements proved above. Those statements must be used exactly as they are. Other statements are theorem proved earlier. They have free variables, and we have a number of variables already defined. Our defined variables must be substituted for the free variables in all all possible ways. If we have d defined variables, and a theorem has f free variables, then there are f^d different substitutions, if we don't care about typing. As we only want to substitute variables of the same type, we will have much less than f^d substitutions. 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. Hmm, that might cause trouble if there are multiple invocations of a theorem Ri in the same by justification. Now we have a large number of actual statements that we want to combine to prove STATEMENT. The theorem statements are all of the form `this ==> that'. So for each theorem statement, we try to build `this' from all the known statements, and if we can, we add `that' to our list of statements. We proceed in this way until the timeout limit is reached. A smart proof assistant may be able to, as miz3 does, to assert there is an inference error, that there is no way to prove STATEMENT from R1, R2, ..., Rn. Does any of this sound right? I'll read what John says in his purple book. But this is a lot like what I do when I write proofs in miz3. -- Best, Bill ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
