[mizar] Shorter proofs of Mizar theorems

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

Hi,

at http://kti.ms.mff.cuni.cz/~urban/MPTP2/snow_shortened.res is a list of 
329 MML theorems for which a shorter proof was found by a combined 
ATP/machine-learning system run on 276 MML articles.

The syntax of the file is [ LengthDifference, Conjecture, NewReferences, 
OldMMLReferences, NewNeededBackground ], so e.g.
[-4, t34_funct_4, 
[t24_funct_4, t32_funct_4], [d1_funct_4, t21_xboole_1, t25_funct_4, 
t83_xboole_1, t90_relat_1, t9_grfunc_1], [commutativity_k2_xboole_0, 
symmetry_r1_xboole_0]]

says that the new proof of FUNCT_4:34 uses 4 MML references less than the 
original MML proof, the new references are FUNCT_4:24 and FUNCT_4:32, and 
the additional facts needed for the new proof were the commutativity of 
XBOOLE_0:func 2 and symmetry of XBOOLE_0: pred 1.

The methodology is described in 
http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp2.ps, section 4.5 and 4.6. The 
new version of the MPTP system used for this is available at 
http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar.gz .

Josef Urban