Automated Reasoning for Mizar
Mizar article (
example article
)
Insert article here
Local article file to upload
URL to fetch article from
Optional vocabulary file to upload (its name will be kept)
URL to fetch vocabulary file from (its name will be kept)
Article name (must not be in the current MML):
MML version:
4.100.1011
4.145.1096
4.160.1126
4.174.1136
4.178.1142
4.166.1132
4.181.1147
Verify
HTMLize
Parallelization:
None (1 CPU)
2 CPUs
3 CPUs
4 CPUs
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)
Nonstandard transformation
HTML mode
TEXT mode