From: Ben Goertzel (ben@webmind.com)
Date: Thu Apr 26 2001 - 11:55:15 MDT
>
> > Mizar syntax can be used for codifying CS knowledge, but, it's
> not specially
> > tuned for it.
>
> That's what I should have said. Even a short Mizar article
> is very difficult
> for me to read as it is. They have theorems expressed in thousands and
> thousands of lines. What I don't know is how many software
> programs exist that
> can read and verify them?
Only one Mizar-PC
We got halfway through writing a Mizar-KNOW converter, and I hope this will
be finished during the next year
Any math-savvy hackers who want to take this project on, let me know. KNOW
is pretty similar to predicate logic (except it's term logic ;), so a
Mizar-PL converter would look about the same as a Mizar-KNOw converter.
Such a converter would allow lots more people to use Mizar in their AI work.
it would be a great public service. and I don't think it's all that hard.
If anyone's interested I can send them the code that the guy who was
previously working on the problem wrote (he was a contractor in Russia, and
quit when we stopped paying people..)
ben
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:36 MDT