[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Otter2Mizar translator
Hi,
I wrote a translator which translates Otter proof objects to Mizar
articles. Last version is at
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/ott2miz/ott2miz.el .
To create .miz and .voc file for each problem, run
emacs -batch -q -l ott2miz.el --eval '(translate-many <indexfile>)' ,
where <indexfile> is in a directory with all problems (proof objects),
and it contains listing of their filenames (without directory).
Emacs v. >= 21 is required.
Problems from the TPTP library solved by Otter (now 2352, sent to me by
Geoff Sutcliffe), together with the corresponding generated Mizar articles
are at http://kti.ms.mff.cuni.cz/~urban/ott2miz/00ALL.tar.gz .
The symbol handling is now very general, the long term objective is to use
this for putting new results found by provers on MPTP translation back
into MML, which will require to have more special symbol handling.
Josef Urban