Re: [mizar] A quote

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

On Thu, 15 Jan 2004, Piotr Rudnicki wrote:

> Of course that getting the formalization time down is a challenge but
> a sizeable data base can be just what we need to meet this challenge.

If computation is involved, you need more than just passive database. And 
if we talk e.g. about geometry or mathematical physics, it is involved 
very frequently. So vice versa, lack of computation capability also 
hinders the construction of the database in such fields.

Josef