[mizar] ATP proof objects for Mizar

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

Hi,

at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/ are initial 35 
Mizar articles which differ from the standard in the clickable "by" 
keyword (or the final ";" of justifications, if "by" is not needed). If it 
is clicked (e.g the first one in arytm_0 is at 
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/_by/arytm_0/29_21.html 
), an MML Query rendering of an ATP proof object for the by-step is shown 
(in more then 90% cases, solvable quickly by E-PROVER; the rest is empty).

The rendering is not yet perfect - e.g. at 
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/_by/binop_1/54_51.html 
it can be seen that we do not do any moving of types to quantifications 
yet.

The paper describing the process is at 
http://kti.ms.mff.cuni.cz/~urban/mizpres.ps . The original ATP proof 
objects can be seen at 
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/_by_res/, and the 
input for MML Query at 
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/_by_dli/ . The MML 
Query can be used to render the input in real time, by passing the URL to 
it in the following way:
http://mmlquery.mizar.org/cgi-bin/mmlquery/dli?url=http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/_by_dli/zfmisc_1/zfmisc_1__1008_9.dli, 
or more interactively at http://mmlquery.mizar.org/mmlquery/dli.html .

Comments and suggestions are much welcome,
Josef Urban