Automated Reasoning for Mizar


Mizar article (example article)
Local article file to upload
URL to fetch article from
Optional vocabulary file to upload (its name will be kept)
Article name (must not be in the current MML):

Verify
HTMLize

Generate ATP problems
Allow ATP calls for hard problems
Call ATP onload on all Mizar-unsolved (only first 10 are attempted)
Do not call ATP onload on Mizar-unsolved
Mizar-unsolved positions (10 at most) to call ATP onload (list of line:column numbers like: 23:7,456:3,789:22)
HTML mode
TEXT mode