[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Mizar Proof Advisor
Proof advisor trained on MML by data mining techniques is running at
http://lipa.ms.mff.cuni.cz/~urban/posdemo.html.
It gets a formula in MML Query constructor format and gives you theorems and definitions
that it evaluates as most promising for proving the formula.
Direct support is added in the last (CVS) version of Mizar mode for Emacs.
The hitrates obtained by 10-fold cross-validation are at
http://lipa.ms.mff.cuni.cz/~urban/hitrate.jpg .
The graph shows how much of the "really needed" references you get as a
function of increasing the advice limit. This may be a bit imprecise,
since "really needed" here means just past proof experience, while the
advisor might be suggesting another feasible proof.
Josef Urban