| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Mizar Proof Advisor is a system trained on MML proofs by data mining techniques. The server 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.
You can have a look at the success hitrates obtained by 10-fold cross-validation at http://lipa.ms.mff.cuni.cz/~urban/hitrate.jpg.
The typical usage in Mizar Mode is to ask for advice on a formula, which you want to prove. Mizar Proof Advisor uses constructor representation, so you have to use Constructor explanations, See section Constructor explanations, for more.
Once you are in the buffer *Constructors list*, use the
command C-c C-c (mizar-ask-advisor) to get the advice.
The number of hits you want Mizar Proof Advisor to send you.
The default value is 30.
Send the contents of the *Constr Explanations* buffer to Mizar Proof Advisor.
Resulting advice is shown in the buffer *Proof Advice*, where normal tag-browsing
keyboard bindings can be used to view the suggested references.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.
