There is just one fly in the ointment as far as I am concerned. It is
simply this. What Babel is attempting to do is a lot less than what
formal mathematical methods are doing.

(snip)

Isn't this exactly what Mizar is doing? Alcor is a front end of Mizar
and quite a user friendly interface is provided.

http://www.google.co.uk/search?hl=en&q=mizar+and+alcor+formal+proof&btnG=Google+Search&meta=&aq=f&oq=

This is the result of a search on formal proof.

http://groups.google.com/group/creatingAI/browse_thread/thread/772ab668e92d79f8

Here is an interesting thread where I have discussed a number of the
principle concepts. The fact of the matter is that everything in
README is provided for by Mizar. Alcor is attempting a verbal output.
Here is some correspondence I have had with Arnold Neumeier at Vienna
University. We were thinking principally in terms of English and
German although other languages will follow.

I feel that Babel should look at proof engines and what they are
attempting before they go any further.

The only predicates that have been set in stone are
those for representing cardinal and ordinal numbers.

Ian Parker wrote:

There is just one fly in the ointment as far as I am concerned. It is
simply this. What Babel is attempting to do is a lot less than what
formal mathematical methods are doing.

In what way is that a problem?  That I'm not going off on some
strange tangent actually sounds quite reassuring to me.

(snip)

Isn't this exactly what Mizar is doing? Alcor is a front end of Mizar
and quite a user friendly interface is provided.

I'd be very surprised if Mizar were the only other system using
a similar notation, given its relationship to predicate logic.

http://www.google.co.uk/search?hl=en&q=mizar+and+alcor+formal+proof&b...

This is the result of a search on formal proof.

http://groups.google.com/group/creatingAI/browse_thread/thread/772ab6...

Here is an interesting thread where I have discussed a number of the
principle concepts. The fact of the matter is that everything in
README is provided for by Mizar. Alcor is attempting a verbal output.
Here is some correspondence I have had with Arnold Neumeier at Vienna
University. We were thinking principally in terms of English and
German although other languages will follow.

OK, I've taken a look at the Mizar home page, and also at the
Wikipedia article.  According to the latter it is closed-source,
which is a pretty fundamental deal-breaker for the application
I'm targetting.

Also, even if the underlying engine could do what's needed, I
get the impression that its field of application is currently
very narrow (ie. mathematics).  If that's correct then I can't
see it bringing much to the table - most of the problems that
I need to solve at this point lie outside that domain.

This is really what I am debating. I think you have far too limited a

I feel that Babel should look at proof engines and what they are
attempting before they go any further.

Always happy to look at alternative approaches, but I'm not
sure what specifically would be useful in this case.

To be clear, it doesn't translate from any natural language,
only to natural languages from BabelScript.

The chemical elements have been implemented (but are not yet
supported) in English, French, Italian, Spanish, Portuguese,
Danish, Welsh and Irish Gaelic. You can generate them thus:

babel-translate -l fr chem:element:iron[noun]

(The required part of speech needs to be specified because this
is not a complete sentence.)

Graham Shaw wrote:

To be clear, it doesn't translate from any natural language,
only to natural languages from BabelScript.

The chemical elements have been implemented (but are not yet
supported) in English, French, Italian, Spanish, Portuguese,
Danish, Welsh and Irish Gaelic. You can generate them thus:

babel-translate -l fr chem:element:iron[noun]

(The required part of speech needs to be specified because this
is not a complete sentence.)

With the help of the supplied specification, each word is thus
translated correctly. But I don't yet capture what kind of
practical applications you envisage for your system, if translation
of natural language sentences isn't the goal. (Sorry for my
poor comprehension capability.)

On 21 June, 15:01, Graham Shaw <gds... at (no spam) riscpkg.org> wrote:
Ian Parker wrote:

OK, I've taken a look at the Mizar home page, and also at the
Wikipedia article. According to the latter it is closed-source,
which is a pretty fundamental deal-breaker for the application
I'm targetting.

http://www.uclic.ucl.ac.uk/people/j.gow/papers/alcor-jar.pdf

I do not think it is a closed system. It is very much a system in
development.

Also, even if the underlying engine could do what's needed, I
get the impression that its field of application is currently
very narrow (ie. mathematics). If that's correct then I can't
see it bringing much to the table - most of the problems that
I need to solve at this point lie outside that domain.

This is really what I am debating. I think you have far too limited a
view of what Mathematics is. If I speak of the Stefan Boltzmann law I
am presenting an entry into a highly formalised system of logic. I
have to say proportionasl to the fourTH (four is absolute nonsense)
power of the absolute temperature.

I feel that Babel should look at proof engines and what they are
attempting before they go any further.
Always happy to look at alternative approaches, but I'm not
sure what specifically would be useful in this case.

Mizar is 30 years old. It seems to me that Babel is going down a path
that is already well trodden. Mizar/Alcor is generally regarded as the
most mature although there are indeed others. Alcor presents the most
natural looking mathematics.

http://www.cl.cam.ac.uk/~jrh13/hol-light/

What I said (or rather, what Wikipedia claimed) is that it is
closed-source, as in, not supplied with source code.

Wikipaedia is not 100% reliable. It if fairly god though. In this case

That would make it incompatible with the Open Source Definition.
Since I'm not in the business of developing non-free software, it
isn't something I would want to use directly.

 >> Also, even if the underlying engine could do what's needed, I
 >> get the impression that its field of application is currently
 >> very narrow (ie. mathematics).  If that's correct then I can't
 >> see it bringing much to the table - most of the problems that
 >> I need to solve at this point lie outside that domain.
 
 > This is really what I am debating. I think you have far too limited a
 > view of what Mathematics is. If I speak of the Stefan Boltzmann law I
 > am presenting an entry into a highly formalised system of logic. I
 > have to say proportionasl to the fourTH (four is absolute nonsense)
 > power of the absolute temperature.

Yes, but are you talking about what it has the potential to do,
or what it can do now?

In other words, does it actually have the dictionaries needed to
translate into a large number of languages across a wide range of
topics?

No, it really only has dictionaries for English. No doubt Arnold will

Not that I have them either, of course, but that's 99% or more
of the problem.  The effort involved in writing a translation
engine pales into insignificance by comparison.

(Even for the little I've done so far, I've spent much more time
reading grammar books than writing code.)

 >>> I feel that Babel should look at proof engines and what they are
 >>> attempting before they go any further.
 >> Always happy to look at alternative approaches, but I'm not
 >> sure what specifically would be useful in this case.
 
 > Mizar is 30 years old. It seems to me that Babel is going down a path
 > that is already well trodden. Mizar/Alcor is generally regarded as the
 > most mature although there are indeed others. Alcor presents the most
 > natural looking mathematics.
 
 >http://www.cl.cam.ac.uk/~jrh13/hol-light/

I'll take a look at both of them to see what can be learned.
Also I note that HOL Light is free software, which helps
significantly.
-

It would be far simpler for a multilingual application to simply have an
array of message format strings, with interpolated parameter values, as
is already common practice. "blah blah %d blah blah %s"

This is in fact (probably) the way Alcor/Mizar or Wolfram would

I worked back in 2005 on a commercial system which supported 22
languages in almost as many character sets, including traditional
Chinese, simplified Chinese, Japanese, Korean, most European languages,
including for example Czech, Swedish, Danish, etc and both Portuguese
and Brazilian Portuguese, as well as the obvious French & German. I'm
afraid the systems which might benefit from Babel have already solved
these issues albeit in a dumb pragmatic fashion, long ago. This system
was tailored to the specific phrases required, rather than attempting
generic translations.

Practical commercial systems must render each phrase in the appropriate
idiom, often tailored to specific variants eg. German vs Switzer-Deutch,
  Portuguese vs Brazilian Portuguese, to be of any practical use.

Any system based on a neutral representational language is adding a
significant additional hurdle to the development effort.

But there is a neutral representation language. It's called a proof

On 22 June, 06:42, Graham Shaw <gds... at (no spam) riscpkg.org> wrote:
What I said (or rather, what Wikipedia claimed) is that it is
closed-source, as in, not supplied with source code.

Wikipaedia is not 100% reliable. It if fairly god though. In this case
what it is claiming is true but slightly misleading. It is indeed NOT
open source, but there are quite a lot of developers who have access
to the code.

What you have to do is convince them that you have got
something to contribute, and negotiate a deal.

This probably wont matter to you but HOL lite is less popular with
mathematicians because the proofs given are less like natural
mathematics than Mizar.