[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] mizar2kif


Hi Ben,

On Sat, 17 Mar 2007, Ben Goertzel wrote:



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.
Good, hope you'll submit your system to the MPTP Challenge (http://www.cs.miami.edu/~tptp/MPTPChallenge/), and write a paper about it to ESARLT (http://www.cs.miami.edu/~geoff/Conferences/ESARLT/). 


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.
Mizar is translated to TPTP by the MPTP export (http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar.gz). TPTP2KIF can be probably achieved through TPTP2X from the TPTP distro (not that there would be many "really running systems" fully implementing KIF (AFAIK)). Also, just for initial learning experiments, the MPTPChallenge problems (http://www.cs.miami.edu/~tptp/MPTPChallenge/MPTPChallenge.tgz) might be enough. 


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?
I hope that MPTP is enough for you, you are welcome to play with it and improve it - there are number of ways how one can "translate" Mizar and its proofs, e.g. with respect to optimizations available in various reasoning systems, and I hardly did the "basic" approach so far. Also Mizar is available in XML-ized format (http://mmlquery.mizar.org/mizardoc/xml/Mizar.html) which solves the low-level technical "loading" issue, and may be also usable e.g. for machine learning (fo some hints read e.g. section 3.5 of http://ktiml.mff.cuni.cz/~urban/mizxml.ps). However it is certainly still "Mizar world", not a standardized well-known format like TPTP. 

Best regards,
Josef Urban