RE: Mizar conversion project...

From: Ben Goertzel (ben@goertzel.org)
Date: Mon Oct 24 2005 - 09:02:37 MDT


Basically, you have to write and have approved a Mizar article to get
admitted to the SUM club.

The questions are then

a)
whether they would be happy to have someone hack their proof-checker into a
converter from Mizar into some other format (such as KIF, my suggestion --
see http://www-ksl.stanford.edu/knowledge-sharing/kif/) and then post the
KIF version of Mizar for AI usage

b)
whether their converter is in such a state that hacking it is actually the
best way to make a Mizar-to-KIF converter (as opposed to just starting from
scratch)

I don't know the answer to either of these questions. I suspect the answer
to b may be that it's easier to start from scratch, but that's just a
suspicion (and perhaps a bias ;-)

-- Ben

> -----Original Message-----
> From: owner-sl4@sl4.org [mailto:owner-sl4@sl4.org]On Behalf Of Herb
> Martin
> Sent: Monday, October 24, 2005 1:52 AM
> To: sl4@sl4.org
> Subject: RE: Mizar conversion project...
>
>
> Supposedly (according to Wikipedia:Mizar_system) only
> members of the SUM (Association of Mizar Users)
> have access to the Pascal source to Mizar.
>
> There is an application here, but the PS fails
> to load in my Ghostscript:
>
> ASSOCIATION OF MIZAR USERS
> <http://mizar.uwb.edu.pl/sum/>
>
>
> The Wikipedia reference is here:
> http://en.wikipedia.org/wiki/Mizar_system
>
> --
> Herb Martin
>
>



This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT