Re: [mizar] MoMM:Most of Math Matches

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Basically yes, but you have to imply all that by 'local equalities'.
That is what the relcprem tool is used for - prune from the inferences 
unnecessary local equalities and constants. 
I am trying to write some doc without much success so far.
I am going to do the same (or almost the same) things with subproofs 
(that means implying by references external to the subproof). The 
'hit count' - how many inferences or subproofs are subsumed by a 
generalized inference or generalized subproof is probably a good measure 
of how useful it is to export the inference/subproof as a theorem.

Josef

On Sat, 7 Dec 2002, Andrzej Trybulec wrote:

> 
> 
> Josef Urban wrote:
> 
> >
> > Besides, there are about 700000 clauses created by logically correct
> > generalization of all of the simple facts (simple justifications)
> > ever proved by Mizar, that can additionally be loaded and used in
> > exactly the same manner.
> >
> 
> What you mean by 'logically correct generalization'. Binding local
> variables? or something more?
> 
> Andrzej Trybulec
>