« Return to Thread: mizar2kif

Re: mizar2kif

by Ben Goertzel :: Rate this Message:

Josef,

Thanks for your reply! However, I'm not sure we are fully understanding
each other.

I agree that the TPTP language has a level of simplicity similar to that
of KIF, so that converting TPTP into KIF wouldn't be a big deal.

And, from the point of view of my own Novamente AI system, writing a
specialized TPTP loader and bypassing KIF wouldn't be a big deal either.

However, I am not sure from your email if the "MPTP export" of Mizar, at
this point, actually exports the **proofs** in the existing Mizar corpus
(Journal of Formalized Mathematics), or just the theorem statements.
Can you clarify?

For my purposes, I need the proofs not just the theorems, as my desire
is to do inductive learning of proof-patterns based on automated
analysis of the proof-corpus.

Thanks
Ben Goertzel
Novamente LLC
ben@...

>
> 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
>

« Return to Thread: mizar2kif