is a system providing hints for a proof of arbitrary Mizar formula, trained on MML proofs by data mining techniques. More detailed description is at http://kti.mff.cuni.cz/~urban/MizarModeDoc/html/MizarMode_11.html and http://kti.mff.cuni.cz/~urban/MPTP/mptp-jar.ps.gz .

The online advisor is running at http://lipa.ms.mff.cuni.cz/~urban/posdemo.html, tho local distro can be downloaded from http://kti.mff.cuni.cz/~urban/MPA/mpadistro.tar.gz

-- JosefUrban - 18 Dec 2004