Bob: >I have found that various people will not even consider >Mizar once they hear that the source for the Mizar proof >checker is not publically available. For a contrasting data point, note that PVS is the most popular proof assistant of today, and it is very much copyrighted, and its source is certainly _not_ easily obtainable too (it took me half a year to get a license). Freek