[mizar] mizar2kif

[Ben Goertzel <ben@goertzel.org>]

Hi all,

I am the leader of an AI project (www.novamente.net) and am interested
to apply my AI system to automated theorem-proving based on a method
of having it ingest the existing corpus of Mizar proofs, inductively infer
"patterns of proof" therefrom, and then use these patterns to guide its
work in further proofs.

However, the first issue confronted along this path is that my AI system
does not possess a Mizar loader.  This is because Mizar's syntax is
bloody complicated!  (Understandably so, because of its design goals.)

Thus, it seems necessary to convert Mizar to some simpler and more standard
format.  A sensible choice would seem to be KIF

http://www.ksl.stanford.edu/knowledge-sharing/kif/

but of course other similarly simple formats would do as well.

My question is whether anyone has created a converter of this sort, or has
thought seriously about it.

If no one has created one, does anyone have an educated estimate regarding
how long this task would take for an individual with suitable background
in mathematics and software engineering?

Thanks
Ben Goertzel
ben@goertzel.org